diff options
| -rw-r--r-- | lib/flags.ml | 1 | ||||
| -rw-r--r-- | lib/flags.mli | 1 | ||||
| -rw-r--r-- | parsing/printer.ml | 15 | ||||
| -rw-r--r-- | parsing/printer.mli | 16 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 5 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 9 |
7 files changed, 25 insertions, 24 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 547e394aa3..e8763bc79f 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -23,7 +23,6 @@ let batch_mode = ref false let debug = ref false let print_emacs = ref false -let print_emacs_safechar = ref false let term_quality = ref false diff --git a/lib/flags.mli b/lib/flags.mli index dd0f33ae4c..f7e3c17597 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -15,7 +15,6 @@ val batch_mode : bool ref val debug : bool ref val print_emacs : bool ref -val print_emacs_safechar : bool ref val term_quality : bool ref diff --git a/parsing/printer.ml b/parsing/printer.ml index 10ccd879ba..e99dc2b1c6 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -27,11 +27,8 @@ open Tacexpr open Store.Field -let emacs_str s alts = - match !Flags.print_emacs, !Flags.print_emacs_safechar with - | true, true -> alts - | true , false -> s - | false,_ -> "" +let emacs_str s = + if !Flags.print_emacs then s else "" (**********************************************************************) (** Terms *) @@ -220,7 +217,7 @@ let pr_context_limit n env = else let pidt = pr_var_decl env d in (i+1, (pps ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253)) "") ++ + str (emacs_str "") ++ pidt))) env ~init:(0,(mt ())) in @@ -229,7 +226,7 @@ let pr_context_limit n env = (fun env d pps -> let pnat = pr_rel_decl env d in (pps ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253)) "") ++ + str (emacs_str "") ++ pnat)) env ~init:(mt ()) in @@ -267,7 +264,7 @@ let default_pr_goal gs = in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253)) "") ++ + str (emacs_str "") ++ str "============================" ++ fnl () ++ thesis ++ str " " ++ pc) ++ fnl () @@ -276,7 +273,7 @@ let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in - str (emacs_str (String.make 1 (Char.chr 253)) "") ++ + str (emacs_str "") ++ str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) diff --git a/parsing/printer.mli b/parsing/printer.mli index b4e0537a5e..cdd2f42770 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -115,11 +115,17 @@ val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds (** Emacs/proof general support - (emacs_str s alts) outputs - - s if emacs mode & unicode allowed, - - alts if emacs mode and & unicode not allowed - - nothing otherwise *) -val emacs_str : string -> string -> string + (emacs_str s) outputs + - s if emacs mode, + - nothing otherwise. + This function was previously used to insert special chars like + [(String.make 1 (Char.chr 253))] to parenthesize sub-parts of the + proof context for proof by pointing. This part of the code is + removed for now because it interacted badly with utf8. We may put + it back some day using some xml-like tags instead of special + chars. See for example the <prompt> tag in the prompt when in + emacs mode. *) +val emacs_str : string -> string (** Backwards compatibility *) diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 5ac3e8e9ed..8ed3ae62d3 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -33,7 +33,7 @@ let pr_goal gs = in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ - str (Printer.emacs_str (String.make 1 (Char.chr 253)) "") ++ + str (Printer.emacs_str "") ++ str "============================" ++ fnl () ++ thesis ++ str " " ++ pc) ++ fnl () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c0f6894674..eda05350b8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -247,8 +247,9 @@ let parse_args arglist = | "-vm" :: rem -> use_vm := true; parse rem | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem - | "-emacs-U" :: rem -> Flags.print_emacs := true; - Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem + | "-emacs-U" :: rem -> + warning "Obsolete option \"-emacs-U\", use -emacs instead."; + Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem | "-unicode" :: rem -> add_require "Utf8_core"; parse rem diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 92e29c0421..699fd12f9d 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -47,13 +47,12 @@ let resynch_buffer ibuf = | _ -> () -(* emacs special character for prompt end (fast) detection. Prefer - (Char.chr 6) since it does not interfere with utf8. For - compatibility we let (Char.chr 249) as default for a while. *) +(* emacs special prompt tag for easy detection. No special character, + to avoid interfering with utf8. Compatibility code removed. *) -let emacs_prompt_startstring() = Printer.emacs_str "" "<prompt>" +let emacs_prompt_startstring() = Printer.emacs_str "<prompt>" -let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "</prompt>" +let emacs_prompt_endstring() = Printer.emacs_str "</prompt>" (* Read a char in an input channel, displaying a prompt at every beginning of line. *) |