diff options
| -rw-r--r-- | parsing/printer.ml | 18 | ||||
| -rw-r--r-- | parsing/printer.mli | 7 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 15 |
3 files changed, 22 insertions, 18 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index a128eb1a7..deaf796ad 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -29,7 +29,11 @@ open Pfedit open Ppconstr open Constrextern -let emacs_str s = if !Options.print_emacs then s else "" +let emacs_str s alts = + match !Options.print_emacs, !Options.print_emacs_safechar with + | true, true -> alts + | true , false -> s + | false,_ -> "" (**********************************************************************) (** Terms *) @@ -210,7 +214,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 (String.make 1 (Char.chr 253)) "") ++ pidt))) env ~init:(0,(mt ())) in @@ -219,7 +223,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 (String.make 1 (Char.chr 253)) "") ++ pnat)) env ~init:(mt ()) in @@ -236,7 +240,7 @@ let pr_restricted_named_context among env = (fun env ((id,_,_) as d) pps -> if true || Idset.mem id among then pps ++ - fnl () ++ str (emacs_str (String.make 1 (Char.chr 253))) ++ + fnl () ++ str (emacs_str (String.make 1 (Char.chr 253)) "") ++ pr_var_decl env d else pps) @@ -246,7 +250,7 @@ let pr_subgoal_metas metas env= let pr_one (meta,typ) = str "?" ++ int meta ++ str " : " ++ hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253))) in + str (emacs_str (String.make 1 (Char.chr 253)) "") in hv 0 (prlist_with_sep mt pr_one metas) (* display complete goal *) @@ -265,7 +269,7 @@ let pr_goal g = in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253))) ++ + str (emacs_str (String.make 1 (Char.chr 253)) "") ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () @@ -273,7 +277,7 @@ let pr_goal g = let pr_concl n g = let env = evar_env g in let pc = pr_ltype_env_at_top env g.evar_concl in - str (emacs_str (String.make 1 (Char.chr 253))) ++ + str (emacs_str (String.make 1 (Char.chr 253)) "") ++ str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc diff --git a/parsing/printer.mli b/parsing/printer.mli index dd2a7bad0..580eec8dc 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -98,8 +98,11 @@ val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds (* Emacs/proof general support *) - -val emacs_str : string -> string +(* (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 (* Backwards compatibility *) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index ac8167f28..f75b8fc68 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -52,12 +52,9 @@ let resynch_buffer ibuf = (Char.chr 6) since it does not interfere with utf8. For compatibility we let (Char.chr 249) as default for a while. *) -let emacs_prompt_startstring() = - if !Options.print_emacs_safechar then "<prompt>" else "" +let emacs_prompt_startstring() = Printer.emacs_str "" "<prompt>" -let emacs_prompt_endstring() = - if !Options.print_emacs_safechar then "</prompt>" - else String.make 1 (Char.chr 249) +let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "</prompt>" (* Read a char in an input channel, displaying a prompt at every beginning of line. *) @@ -230,9 +227,9 @@ let make_emacs_prompt() = * or after a Drop. *) let top_buffer = let pr() = - Printer.emacs_str (emacs_prompt_startstring()) + emacs_prompt_startstring() ^ make_prompt() - ^ Printer.emacs_str (make_emacs_prompt()) + ^ make_emacs_prompt() in { prompt = pr; str = ""; @@ -244,9 +241,9 @@ let top_buffer = let set_prompt prompt = top_buffer.prompt <- (fun () -> - Printer.emacs_str (emacs_prompt_startstring()) + emacs_prompt_startstring() ^ prompt () - ^ Printer.emacs_str (emacs_prompt_endstring())) + ^ emacs_prompt_endstring()) (* Removes and prints the location of the error. The following exceptions need not be located. *) |