diff options
Diffstat (limited to 'parsing')
-rw-r--r-- | parsing/printer.ml | 18 | ||||
-rw-r--r-- | parsing/printer.mli | 7 |
2 files changed, 16 insertions, 9 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 *) |