From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 1 Jul 2010 17:21:14 +0200 Subject: Imported Upstream version 8.2pl2+dfsg --- parsing/g_decl_mode.ml4 | 4 ++-- parsing/g_intsyntax.ml | 10 ++++++---- parsing/g_vernac.ml4 | 4 +++- parsing/lexer.ml4 | 25 +++++++++++++++---------- parsing/pptactic.ml | 4 ++-- 5 files changed, 28 insertions(+), 19 deletions(-) (limited to 'parsing') diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 index 61c3474d..35fc064b 100644 --- a/parsing/g_decl_mode.ml4 +++ b/parsing/g_decl_mode.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*) -(* $Id: g_decl_mode.ml4 10739 2008-04-01 14:45:20Z herbelin $ *) +(* $Id: g_decl_mode.ml4 12414 2009-10-25 18:50:41Z corbinea $ *) open Decl_expr @@ -220,7 +220,7 @@ GLOBAL: proof_instr; intro_step: [[ IDENT "suppose" ; h=assume_clause -> Psuppose h | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ; - po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; + po=OPT[ "with"; p=LIST1 hyp SEP ","-> p ] ; ho=OPT[ IDENT "and" ; h=suppose_clause -> h ] -> Pcase (none_is_empty po,c,none_is_empty ho) | "let" ; v=let_vars -> Plet v diff --git a/parsing/g_intsyntax.ml b/parsing/g_intsyntax.ml index a589ccf1..64fa0b49 100644 --- a/parsing/g_intsyntax.ml +++ b/parsing/g_intsyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: g_intsyntax.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: g_intsyntax.ml 12509 2009-11-12 15:52:50Z letouzey $ i*) (* digit-based syntax for int31, bigN bigZ and bigQ *) @@ -92,13 +92,15 @@ let bigZ_neg = ConstructRef ((bigZ_id "t_",0),2) (*bigQ stuff*) let bigQ_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "BigQ"] -let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake_base"] +let qmake_module = ["Coq"; "Numbers"; "Rational"; "BigQ"; "QMake"] let bigQ_path = make_path (bigQ_module@["BigQ"]) "t" (* big ugly hack bis *) -let bigQ_id = make_kn qmake_module +let bigQ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigQ_module)), + Names.mk_label "BigQ")), + [], Names.id_of_string id) : Names.kernel_name) let bigQ_scope = "bigQ_scope" -let bigQ_z = ConstructRef ((bigQ_id "q_type",0),1) +let bigQ_z = ConstructRef ((bigQ_id "t_",0),1) (*** Definition of the Non_closed exception, used in the pretty printing ***) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b2d67e1c..f727dfea 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_vernac.ml4 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: g_vernac.ml4 13197 2010-06-25 22:36:17Z letouzey $ *) open Pp @@ -663,6 +663,8 @@ GEXTEND Gram check_command: (* TODO: rapprocher Eval et Check *) [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> fun g -> VernacCheckMayEval (Some r, g, c) + | IDENT "Compute"; c = lconstr -> + fun g -> VernacCheckMayEval (Some Rawterm.CbvVm, g, c) | IDENT "Check"; c = lconstr -> fun g -> VernacCheckMayEval (None, g, c) ] ] ; diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 2633386f..52b5ede7 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: lexer.ml4 11786 2009-01-14 13:07:34Z herbelin $ i*) +(*i $Id: lexer.ml4 12891 2010-03-30 11:40:02Z herbelin $ i*) (*i camlp4use: "pr_o.cmo" i*) @@ -91,6 +91,14 @@ let error_utf8 cs = Stream.junk cs; (* consume the char to avoid read it and fail again *) err (bp, bp+1) Illegal_character +let utf8_char_size cs = function + (* Utf8 leading byte *) + | '\x00'..'\x7F' -> 1 + | '\xC0'..'\xDF' -> 2 + | '\xE0'..'\xEF' -> 3 + | '\xF0'..'\xF7' -> 4 + | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> error_utf8 cs + let njunk n = Util.repeat n Stream.junk let check_utf8_trailing_byte cs c = @@ -355,14 +363,8 @@ and progress_utf8 last nj n c tt cs = with Not_found -> last -and progress_from_byte last nj tt cs = function - (* Utf8 leading byte *) - | '\x00'..'\x7F' as c -> progress_utf8 last nj 1 c tt cs - | '\xC0'..'\xDF' as c -> progress_utf8 last nj 2 c tt cs - | '\xE0'..'\xEF' as c -> progress_utf8 last nj 3 c tt cs - | '\xF0'..'\xF7' as c -> progress_utf8 last nj 4 c tt cs - | _ (* '\x80'..\xBF'|'\xF8'..'\xFF' *) -> - error_utf8 cs +and progress_from_byte last nj tt cs c = + progress_utf8 last nj (utf8_char_size cs c) c tt cs (* Must be a special token *) let process_chars bp c cs = @@ -370,7 +372,10 @@ let process_chars bp c cs = let ep = Stream.count cs in match t with | Some t -> (("", t), (bp, ep)) - | None -> err (bp, ep) Undefined_token + | None -> + let ep' = bp + utf8_char_size cs c in + njunk (ep' - ep) cs; + err (bp, ep') Undefined_token let parse_after_dollar bp = parser diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 3b433498..f52ebc76 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pptactic.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: pptactic.ml 12581 2009-12-13 15:02:33Z herbelin $ *) open Pp open Names @@ -378,7 +378,7 @@ let pr_as_ipat = function let pr_as_name = function | Anonymous -> mt () - | Name id -> str "as " ++ pr_lident (dummy_loc,id) + | Name id -> str " as " ++ pr_lident (dummy_loc,id) let pr_pose_as_style prc na c = spc() ++ prc c ++ pr_as_name na -- cgit v1.2.3