removed unused info channel;
renamed Output.has_mode to print_mode_active;
cleaned-up Output functions;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Apr 04 00:11:22 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Apr 04 00:11:23 2007 +0200
@@ -23,7 +23,7 @@
val thm_depsN = "thm_deps"; (*meta-information about theorem deps*)
fun special oct =
- if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
+ if print_mode_active pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
else oct_char oct;
@@ -35,7 +35,7 @@
| xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
fun xsymbols_output s =
- if Output.has_mode Symbol.xsymbolsN andalso exists_string (equal "\\") s then
+ if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
let val syms = Symbol.explode s
in (implode (map xsym_output syms), real (Symbol.length syms)) end
else Symbol.default_output s;
@@ -100,17 +100,16 @@
(* messages and notification *)
fun decorate bg en prfx =
- writeln_default o enclose bg en o prefix_lines prfx;
+ Output.writeln_default o enclose bg en o prefix_lines prfx;
fun setup_messages () =
- (writeln_fn := (fn s => decorate "" "" "" s);
- priority_fn := (fn s => decorate (special "360") (special "361") "" s);
- tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
- info_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
- debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
- warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
- error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
- panic_fn := (fn s => decorate (special "364") (special "365") "!!! " s));
+ (Output.writeln_fn := (fn s => decorate "" "" "" s);
+ Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
+ Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
+ Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
+ Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
+ Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
+ Output.panic_fn := (fn s => decorate (special "364") (special "365") "!!! " s));
fun emacs_notify s = decorate (special "360") (special "361") "" s;
@@ -213,7 +212,7 @@
emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
fun tell_thm_deps ths =
- if Output.has_mode thm_depsN then
+ if print_mode_active thm_depsN then
let
val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
val deps = Symtab.keys (fold Proofterm.thms_of_proof'
@@ -279,10 +278,10 @@
Output.panic "No Proof General interface support for Isabelle/classic mode."
| init true =
(! initialized orelse
- (setmp warning_fn (K ()) init_outer_syntax ();
+ (Output.no_warnings init_outer_syntax ();
setup_xsymbols_output ();
setup_messages ();
- ProofGeneralPgip.init_pgip_channel (! priority_fn);
+ ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
setup_state ();
setup_thy_loader ();
setup_present_hook ();
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Apr 04 00:11:22 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Apr 04 00:11:23 2007 +0200
@@ -138,7 +138,7 @@
fun matching_pgip_id id = (id = !pgip_id)
-val output_xml_fn = ref writeln_default
+val output_xml_fn = ref Output.writeln_default
fun output_xml s = (!output_xml_fn) (XML.string_of_tree s); (* TODO: string buffer *)
fun issue_pgip_rawtext str =
@@ -209,14 +209,13 @@
can't be written without newlines. *)
fun setup_messages () =
- (writeln_fn := (fn s => normalmsg Message Normal false s);
- priority_fn := (fn s => normalmsg Message Normal true s);
- tracing_fn := (fn s => normalmsg Message Tracing false s);
- info_fn := (fn s => errormsg Info s);
- warning_fn := (fn s => errormsg Warning s);
- error_fn := (fn s => errormsg Fatal s);
- panic_fn := (fn s => errormsg Panic s);
- debug_fn := (fn s => errormsg Debug s));
+ (Output.writeln_fn := (fn s => normalmsg Message Normal false s);
+ Output.priority_fn := (fn s => normalmsg Message Normal true s);
+ Output.tracing_fn := (fn s => normalmsg Message Tracing false s);
+ Output.warning_fn := (fn s => errormsg Warning s);
+ Output.error_fn := (fn s => errormsg Fatal s);
+ Output.panic_fn := (fn s => errormsg Panic s);
+ Output.debug_fn := (fn s => errormsg Debug s));
fun nonfatal_error s = errormsg Nonfatal s;
fun log_msg s = errormsg Log s;
@@ -429,8 +428,8 @@
preferences :=
(!preferences |> Preferences.set_default ("show-question-marks","false")
|> Preferences.remove "show-question-marks" (* we use markup, not ?s *)
- |> Preferences.remove "theorem-dependencies" (* set internally *)
- |> Preferences.remove "full-proofs") (* set internally *)
+ |> Preferences.remove "theorem-dependencies" (* set internally *)
+ |> Preferences.remove "full-proofs") (* set internally *)
@@ -526,28 +525,28 @@
fun set_proverflag_pgmlsymbols b =
(pgmlsymbols_flag := b;
change print_mode
- (fn mode =>
+ (fn mode =>
remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else [])))
fun set_proverflag_thmdeps b =
(show_theorem_dependencies := b;
proofs := (if b then 1 else 2))
-fun startquiet vs = set_proverflag_quiet true; (* TO BE REMOVED *)
+fun startquiet vs = set_proverflag_quiet true; (* TO BE REMOVED *)
fun stopquiet vs = set_proverflag_quiet false; (* TO BE REMOVED *)
fun pgmlsymbolson vs = set_proverflag_pgmlsymbols true; (* TO BE REMOVED *)
fun pgmlsymbolsoff vs = set_proverflag_pgmlsymbols false; (* TO BE REMOVED *)
fun setproverflag (Setproverflag vs) =
let
- val flagname = #flagname vs
- val value = #value vs
+ val flagname = #flagname vs
+ val value = #value vs
in
- (case flagname of
- "quiet" => set_proverflag_quiet value
- | "pgmlsymbols" => set_proverflag_pgmlsymbols value
- | "metainfo:thmdeps" => set_proverflag_thmdeps value
- | _ => log_msg ("Unrecognised prover control flag: " ^ (quote flagname) ^ " ignored."))
+ (case flagname of
+ "quiet" => set_proverflag_quiet value
+ | "pgmlsymbols" => set_proverflag_pgmlsymbols value
+ | "metainfo:thmdeps" => set_proverflag_thmdeps value
+ | _ => log_msg ("Unrecognised prover control flag: " ^ (quote flagname) ^ " ignored."))
end
@@ -604,7 +603,7 @@
| SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
(thms_of_thy prf))
val qualified_thms_of_thy = (* for global query with single response *)
- (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory;
+ (map fst) o NameSpace.dest_table o PureThy.theorems_of o ThyInfo.get_theory;
(* da: this version is equivalent to my previous, but splits up theorem sets with names
that I can't get to access later with get_thm. Anyway, would rather use sets.
Is above right way to get qualified names in that case? Filtering required again?
@@ -699,35 +698,33 @@
val topthy = Toplevel.theory_of o Toplevel.get_state
- (* Decompose qualified name. FIXME: Should be a better way of doing this *)
- fun splitthy id =
- let
- val comps = scanwords (not o (curry op= ".")) (explode id)
- in case comps of
- (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
- | [plainid] => (topthy(),plainid)
- | _ => raise Toplevel.UNDEF (* assert false *)
- end
-
+ fun splitthy id =
+ let val comps = NameSpace.explode id
+ in case comps of
+ (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
+ | [plainid] => (topthy(),plainid)
+ | _ => raise Toplevel.UNDEF (* assert false *)
+ end
+
fun idvalue strings =
issue_pgip (Idvalue { thyname=thyname, objtype=objtype, name=name,
- text=[XML.Elem("pgmltext",[],
- map XML.Rawtext strings)] })
+ text=[XML.Elem("pgmltext",[],
+ map XML.Rawtext strings)] })
- fun string_of_thm th = Output.output
- (Pretty.string_of
- (Display.pretty_thm_aux
- (Sign.pp (Thm.theory_of_thm th))
- false (* quote *)
- false (* show hyps *)
- [] (* asms *)
- th))
+ fun string_of_thm th = Output.output
+ (Pretty.string_of
+ (Display.pretty_thm_aux
+ (Sign.pp (Thm.theory_of_thm th))
+ false (* quote *)
+ false (* show hyps *)
+ [] (* asms *)
+ th))
fun strings_of_thm (thy, name) = map string_of_thm (get_thms thy (Name name))
- val string_of_thy = Output.output o
- Pretty.string_of o (ProofDisplay.pretty_full_theory false)
+ val string_of_thy = Output.output o
+ Pretty.string_of o (ProofDisplay.pretty_full_theory false)
in
case (thyname, objtype) of
(_,ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
@@ -1058,7 +1055,7 @@
let
val ready' = (process_pgip_tree pgip)
handle PGIP_QUIT => raise PGIP_QUIT
- | e => (handler (e,SOME src'); true)
+ | e => (handler (e,SOME src'); true)
in
loop ready' src'
end
@@ -1111,10 +1108,10 @@
Output.panic "No Proof General interface support for Isabelle/classic mode."
| init_pgip true =
(! initialized orelse
- (setmp warning_fn (K ()) init_outer_syntax ();
+ (Output.no_warnings init_outer_syntax ();
PgipParser.init ();
setup_preferences_tweak ();
- setup_proofgeneral_output ();
+ setup_proofgeneral_output ();
setup_messages ();
setup_state ();
setup_thy_loader ();
@@ -1131,7 +1128,7 @@
(** Out-of-loop PGIP commands (for Emacs hybrid mode) **)
local
- val pgip_output_channel = ref writeln_default
+ val pgip_output_channel = ref Output.writeln_default
in
(* Set recipient for PGIP results *)