diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide/coq.ml | 3 | ||||
| -rw-r--r-- | ide/coqide/coq_lex.mll | 74 | ||||
| -rw-r--r-- | ide/coqide/idetop.ml | 6 | ||||
| -rw-r--r-- | ide/coqide/protocol/serialize.ml | 5 | ||||
| -rw-r--r-- | ide/coqide/protocol/serialize.mli | 1 | ||||
| -rw-r--r-- | ide/coqide/protocol/xmlprotocol.ml | 18 |
6 files changed, 47 insertions, 60 deletions
diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 6e5d57c9a5..1167b8199e 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -545,6 +545,7 @@ struct let coercions = BoolOpt ["Printing"; "Coercions"] let raw_matching = BoolOpt ["Printing"; "Matching"] let notations = BoolOpt ["Printing"; "Notations"] + let parentheses = BoolOpt ["Printing"; "Parentheses"] let all_basic = BoolOpt ["Printing"; "All"] let existential = BoolOpt ["Printing"; "Existential"; "Instances"] let universes = BoolOpt ["Printing"; "Universes"] @@ -559,7 +560,7 @@ struct { opts = [raw_matching]; init = true; label = "Display raw _matching expressions" }; { opts = [notations]; init = true; label = "Display _notations" }; - { opts = [notations]; init = true; label = "Display _parentheses" }; + { opts = [parentheses]; init = false; label = "Display _parentheses" }; { opts = [all_basic]; init = false; label = "Display _all basic low-level contents" }; { opts = [existential]; init = false; diff --git a/ide/coqide/coq_lex.mll b/ide/coqide/coq_lex.mll index a65954d566..5d5e5f0e14 100644 --- a/ide/coqide/coq_lex.mll +++ b/ide/coqide/coq_lex.mll @@ -50,52 +50,40 @@ and comment = parse | utf8_extra_byte { incr utf8_adjust; comment lexbuf } | _ { comment lexbuf } -and quotation o c n l = parse +and quotation n l = parse | eof { raise Unterminated } -| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf } -| _ { - let x = Lexing.lexeme lexbuf in - if x = o then quotation_nesting o c n l 1 lexbuf - else if x = c then - if n = 1 && l = 1 then () - else quotation_closing o c n l 1 lexbuf - else quotation o c n l lexbuf -} +| utf8_extra_byte { incr utf8_adjust; quotation n l lexbuf } +| "{" { quotation_nesting n l 1 lexbuf } +| "}" { quotation_closing n l 1 lexbuf } +| _ { quotation n l lexbuf } -and quotation_nesting o c n l v = parse +and quotation_nesting n l v = parse | eof { raise Unterminated } -| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf } -| _ { - let x = Lexing.lexeme lexbuf in - if x = o then - if n = v+1 then quotation o c n (l+1) lexbuf - else quotation_nesting o c n l (v+1) lexbuf - else if x = c then quotation_closing o c n l 1 lexbuf - else quotation o c n l lexbuf +| utf8_extra_byte { incr utf8_adjust; quotation n l lexbuf } +| "{" { + if n = v+1 then quotation n (l+1) lexbuf + else quotation_nesting n l (v+1) lexbuf } +| "}" { quotation_closing n l 1 lexbuf } +| _ { quotation n l lexbuf } -and quotation_closing o c n l v = parse +and quotation_closing n l v = parse | eof { raise Unterminated } -| utf8_extra_byte { incr utf8_adjust; quotation o c n l lexbuf } -| _ { - let x = Lexing.lexeme lexbuf in - if x = c then - if n = v+1 then - if l = 1 then () - else quotation o c n (l-1) lexbuf - else quotation_closing o c n l (v+1) lexbuf - else if x = o then quotation_nesting o c n l 1 lexbuf - else quotation o c n l lexbuf +| utf8_extra_byte { incr utf8_adjust; quotation n l lexbuf } +| "}" { + if n = v+1 then + if l = 1 then () + else quotation n (l-1) lexbuf + else quotation_closing n l (v+1) lexbuf } +| "{" { quotation_nesting n l 1 lexbuf } +| _ { quotation n l lexbuf } -and quotation_start o c n = parse +and quotation_start n = parse | eof { raise Unterminated } -| utf8_extra_byte { incr utf8_adjust; quotation o c n 1 lexbuf } -| _ { - let x = Lexing.lexeme lexbuf in - if x = o then quotation_start o c (n+1) lexbuf - else quotation o c n 1 lexbuf -} +| utf8_extra_byte { incr utf8_adjust; quotation n 1 lexbuf } +| "{" { quotation_start (n+1) lexbuf } +| _ { quotation n 1 lexbuf } (** NB : [mkiter] should be called on increasing offsets *) @@ -130,16 +118,8 @@ and sentence initial stamp = parse if initial then stamp (utf8_lexeme_start lexbuf + String.length (Lexing.lexeme lexbuf) - 1) Tags.Script.sentence; sentence initial stamp lexbuf } - | ['a'-'z' 'A'-'Z'] ":{" { - quotation_start "{" "}" 1 lexbuf; - sentence false stamp lexbuf - } - | ['a'-'z' 'A'-'Z'] ":[" { - quotation_start "[" "]" 1 lexbuf; - sentence false stamp lexbuf - } - | ['a'-'z' 'A'-'Z'] ":(" { - quotation_start "(" ")" 1 lexbuf; + | ['a'-'z' 'A'-'Z'] ":{{" { + quotation_start 2 lexbuf; sentence false stamp lexbuf } | space+ { diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 2be8f862ea..297dc3a706 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -220,12 +220,12 @@ let process_goal_diffs diff_goal_map oldp nsigma ng = let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in { Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng } -let export_pre_goals Proof.{ sigma; goals; stack; shelf; given_up } process = +let export_pre_goals Proof.{ sigma; goals; stack } process = let process = List.map (process sigma) in { Interface.fg_goals = process goals ; Interface.bg_goals = List.(map (fun (lg,rg) -> process lg, process rg)) stack - ; Interface.shelved_goals = process shelf - ; Interface.given_up_goals = process given_up + ; Interface.shelved_goals = process @@ Evd.shelf sigma + ; Interface.given_up_goals = process (Evar.Set.elements @@ Evd.given_up sigma) } let goals () = diff --git a/ide/coqide/protocol/serialize.ml b/ide/coqide/protocol/serialize.ml index bdbec5b30f..6a0a3d7f5d 100644 --- a/ide/coqide/protocol/serialize.ml +++ b/ide/coqide/protocol/serialize.ml @@ -35,6 +35,11 @@ let singleton = function | l -> raise (Marshal_error ("singleton",PCData ("list of length " ^ string_of_int (List.length l)))) +let empty = function + | [] -> () + | l -> raise (Marshal_error + ("empty",PCData ("list of length " ^ string_of_int (List.length l)))) + let raw_string = function | [] -> "" | [PCData s] -> s diff --git a/ide/coqide/protocol/serialize.mli b/ide/coqide/protocol/serialize.mli index 5d88defe55..9d09b81d1e 100644 --- a/ide/coqide/protocol/serialize.mli +++ b/ide/coqide/protocol/serialize.mli @@ -16,6 +16,7 @@ val massoc: string -> (string * string) list -> string val constructor: string -> string -> xml list -> xml val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b val singleton: 'a list -> 'a +val empty: 'a list -> unit val raw_string: xml list -> string val of_unit: unit -> xml val to_unit: xml -> unit diff --git a/ide/coqide/protocol/xmlprotocol.ml b/ide/coqide/protocol/xmlprotocol.ml index 0780f03903..6a33ff8abc 100644 --- a/ide/coqide/protocol/xmlprotocol.ml +++ b/ide/coqide/protocol/xmlprotocol.ml @@ -43,7 +43,7 @@ let to_search_cst = do_match "search_cst" (fun s args -> match s with | "type_pattern" -> Type_Pattern (to_string (singleton args)) | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) | "in_module" -> In_Module (to_list to_string (singleton args)) - | "include_blacklist" -> Include_Blacklist + | "include_blacklist" -> empty args; Include_Blacklist | x -> raise (Marshal_error("search",PCData x))) let of_coq_object f ans = @@ -103,14 +103,14 @@ let to_routeid = function let of_routeid i = Element ("route_id",["val",string_of_int i],[]) let of_box (ppb : Pp.block_type) = let open Pp in match ppb with - | Pp_hbox i -> constructor "ppbox" "hbox" [of_int i] + | Pp_hbox -> constructor "ppbox" "hbox" [] | Pp_vbox i -> constructor "ppbox" "vbox" [of_int i] | Pp_hvbox i -> constructor "ppbox" "hvbox" [of_int i] | Pp_hovbox i -> constructor "ppbox" "hovbox" [of_int i] let to_box = let open Pp in do_match "ppbox" (fun s args -> match s with - | "hbox" -> Pp_hbox (to_int (singleton args)) + | "hbox" -> empty args; Pp_hbox | "vbox" -> Pp_vbox (to_int (singleton args)) | "hvbox" -> Pp_hvbox (to_int (singleton args)) | "hovbox" -> Pp_hovbox (to_int (singleton args)) @@ -132,7 +132,7 @@ let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with let rec to_pp xpp = let open Pp in Pp.unrepr @@ do_match "ppdoc" (fun s args -> match s with - | "empty" -> Ppcmd_empty + | "empty" -> empty args; Ppcmd_empty | "string" -> Ppcmd_string (to_string (singleton args)) | "glue" -> Ppcmd_glue (to_list to_pp (singleton args)) | "box" -> let (bt,s) = to_pair to_box to_pp (singleton args) in @@ -883,11 +883,11 @@ let of_message_level = function | Error -> Serialize.constructor "message_level" "error" [] let to_message_level = Serialize.do_match "message_level" (fun s args -> match s with - | "debug" -> Debug - | "info" -> Info - | "notice" -> Notice - | "warning" -> Warning - | "error" -> Error + | "debug" -> empty args; Debug + | "info" -> empty args; Info + | "notice" -> empty args; Notice + | "warning" -> empty args; Warning + | "error" -> empty args; Error | x -> raise Serialize.(Marshal_error("error level",PCData x))) let of_message lvl loc msg = |