diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-18 11:49:25 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-18 11:53:55 +0100 |
commit | 80cfb61c8c497a2d33a6b47fcdaa9d071223a502 (patch) | |
tree | 4371040b97d39647f9e8679e4d8e8a1a6b077a3a /parsing | |
parent | 0f5e89ec54bc613f59ce971e6a95ed1161ffc37b (diff) | |
parent | bdcf5b040b975a179fe9b2889fea0d38ae4689df (diff) |
Merge branch 'v8.6'
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/cLexer.ml4 | 24 | ||||
-rw-r--r-- | parsing/g_proofs.ml4 | 10 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 39 | ||||
-rw-r--r-- | parsing/pcoq.ml | 1 | ||||
-rw-r--r-- | parsing/pcoq.mli | 1 |
5 files changed, 33 insertions, 42 deletions
diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 69e4eb8d2..003fb6789 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -408,24 +408,6 @@ let comment_stop ep = comment_begin := None; between_commands := false -(* Does not unescape!!! *) -let rec comm_string loc bp = parser - | [< ''"' >] -> push_string "\""; loc - | [< ''\\'; loc = - (parser [< ' ('"' | '\\' as c) >] -> - let () = match c with - | '"' -> real_push_char c - | _ -> () - in - real_push_char c; loc - | [< >] -> real_push_char '\\'; loc); s >] - -> comm_string loc bp s - | [< _ = Stream.empty >] ep -> - let loc = set_loc_pos loc bp ep in - err loc Unterminated_string - | [< ''\n' as c; s >] ep -> real_push_char c; comm_string (bump_loc_line loc ep) bp s - | [< 'c; s >] -> real_push_char c; comm_string loc bp s - let rec comment loc bp = parser bp2 | [< ''('; loc = (parser @@ -437,11 +419,7 @@ let rec comment loc bp = parser bp2 | [< '')' >] -> push_string "*)"; loc | [< s >] -> real_push_char '*'; comment loc bp s >] -> loc | [< ''"'; s >] -> - let loc = - (* In beautify mode, the lexing differs between strings in comments and - regular strings (e.g. escaping). It seems wrong. *) - if !Flags.beautify then (push_string"\""; comm_string loc bp2 s) - else fst (string loc ~comm_level:(Some 0) bp2 0 s) + let loc = fst (string loc ~comm_level:(Some 0) bp2 0 s) in comment loc bp s | [< _ = Stream.empty >] ep -> diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 2adbf300e..4c5280538 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -98,10 +98,9 @@ GEXTEND Gram (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; - pri = OPT [ "|"; i = natural -> i ]; - dbnames = opt_hintbases -> + info = hint_info; dbnames = opt_hintbases -> VernacHints (false,dbnames, - HintsResolve (List.map (fun x -> (pri, true, x)) lc)) + HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; obsolete_locality: [ [ IDENT "Local" -> true | -> false ] ] @@ -111,9 +110,8 @@ GEXTEND Gram | c = constr -> HintsConstr c ] ] ; hint: - [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; - pri = OPT [ "|"; i = natural -> i ] -> - HintsResolve (List.map (fun x -> (pri, true, x)) lc) + [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info -> + HintsResolve (List.map (fun x -> (info, true, x)) lc) | IDENT "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true) | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (lc, false) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 7bc5bfca3..b3233f8f0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -582,7 +582,7 @@ let warn_deprecated_implicit_arguments = (* Extensions: implicits, coercions, etc. *) GEXTEND Gram - GLOBAL: gallina_ext instance_name; + GLOBAL: gallina_ext instance_name hint_info; gallina_ext: [ [ (* Transparent and Opaque *) @@ -635,17 +635,20 @@ GEXTEND Gram | IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] ; + info = hint_info ; props = [ ":="; "{"; r = record_declaration; "}" -> Some (true,r) | ":="; c = lconstr -> Some (false,c) | -> None ] -> - VernacInstance (false,snd namesup,(fst namesup,expl,t),props,pri) + VernacInstance (false,snd namesup,(fst namesup,expl,t),props,info) | IDENT "Existing"; IDENT "Instance"; id = global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances ([id], pri) + info = hint_info -> + VernacDeclareInstances [id, info] + | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global; - pri = OPT [ "|"; i = natural -> i ] -> - VernacDeclareInstances (ids, pri) + pri = OPT [ "|"; i = natural -> i ] -> + let info = { hint_priority = pri; hint_pattern = None } in + let insts = List.map (fun i -> (i, info)) ids in + VernacDeclareInstances insts | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is @@ -786,6 +789,11 @@ GEXTEND Gram (Option.default [] sup) | -> ((!@loc, Anonymous), None), [] ] ] ; + hint_info: + [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> + { hint_priority = i; hint_pattern = pat } + | -> { hint_priority = None; hint_pattern = None } ] ] + ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] ; @@ -807,8 +815,8 @@ GEXTEND Gram (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; - pri = OPT [ "|"; i = natural -> i ] -> - VernacInstance (true, snd namesup, (fst namesup, expl, t), None, pri) + info = hint_info -> + VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) (* System directory *) | IDENT "Pwd" -> VernacChdir None @@ -866,11 +874,16 @@ GEXTEND Gram | "Set"; table = option_table; v = option_value -> begin match v with | StringValue s -> - let (last, prefix) = List.sep_last table in - if String.equal last "Append" && not (List.is_empty prefix) then - VernacSetAppendOption (prefix, s) + (* We make a special case for warnings because appending is their + natural semantics *) + if CString.List.equal table ["Warnings"] then + VernacSetAppendOption (table, s) else - VernacSetOption (table, v) + let (last, prefix) = List.sep_last table in + if String.equal last "Append" && not (List.is_empty prefix) then + VernacSetAppendOption (prefix, s) + else + VernacSetOption (table, v) | _ -> VernacSetOption (table, v) end | "Set"; table = option_table -> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9787af826..c5823440a 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -338,6 +338,7 @@ module Vernac_ = let vernac_eoi = eoi_entry vernac let rec_definition = gec_vernac "Vernac.rec_definition" let red_expr = make_gen_entry utactic "red_expr" + let hint_info = gec_vernac "hint_info" (* Main vernac entry *) let main_entry = Gram.entry_create "vernac" let noedit_mode = gec_vernac "noedit_command" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 55868900a..77884fb1c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -189,6 +189,7 @@ module Vernac_ : val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry val red_expr : raw_red_expr Gram.entry + val hint_info : Vernacexpr.hint_info_expr Gram.entry end (** The main entry: reads an optional vernac command *) |