--- a/src/Pure/proof_general.ML Mon Aug 16 17:56:07 2004 +0200
+++ b/src/Pure/proof_general.ML Mon Aug 16 18:05:41 2004 +0200
@@ -2,7 +2,25 @@
ID: $Id$
Author: David Aspinall and Markus Wenzel
-Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk).
+Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk)
+Includes support for PGIP control language for Isabelle/Isar.
+
+===========================================================================
+NOTE: With this version you will lose support for the Isabelle
+preferences menu in the currently released version of Proof General (3.5).
+No other changes should be visible in the Emacs interface.
+
+If the loss of preferences is a serious problem, please use a "sticky"
+check-out of the previous version of this file, version 1.27.
+
+A version of Proof General which supports the new PGIP format for
+preferences will be available shortly.
+===========================================================================
+
+STATUS: this version is an interim experimental version that was
+used from 07.2003-08.2004 for the development of PGIP 1.X. This will
+soon be replaced by a version for PGIP 2.X.
+
*)
signature PROOF_GENERAL =
@@ -12,7 +30,12 @@
val try_update_thy_only: string -> unit
val inform_file_retracted: string -> unit
val inform_file_processed: string -> unit
- val options: (string * (string * (string * (unit -> string) * (string -> unit)))) list ref
+ val preferences:
+ (string *
+ (string *
+ (string *
+ (string * (string * (unit -> string)) *
+ (string -> unit)))) list) list ref
val process_pgip: string -> unit
val thms_containing: string list -> unit
val help: unit -> unit
@@ -21,25 +44,35 @@
val repeat_undo: int -> unit
val isa_restart: unit -> unit
val full_proofs: bool -> unit
+ val isarcmd: string -> unit
val init: bool -> unit
+ val init_pgip: bool -> unit
val write_keywords: string -> unit
end;
-structure ProofGeneral: PROOF_GENERAL =
+structure ProofGeneral : PROOF_GENERAL =
struct
+(* PGIP messaging mode (independent of PGML output) *)
+
+val pgip_active = ref false;
+val pgip_emacs_compatibility_flag = ref false;
+
+fun pgip () = (!pgip_active);
+fun pgip_emacs_compatibility () = (!pgip_emacs_compatibility_flag);
+
+
(* print modes *)
-val proof_generalN = "ProofGeneral";
-val xsymbolsN = "xsymbols";
-val thm_depsN = "thm_deps";
+val proof_generalN = "ProofGeneral"; (* token markup (colouring vars, etc.) *)
+val xsymbolsN = Symbol.xsymbolsN; (* XSymbols symbols *)
+val pgmlN = "PGML"; (* XML escapes and PGML symbol elements *)
+val pgmlatomsN = "PGMLatoms"; (* variable kind decorations *)
+val thm_depsN = "thm_deps"; (* meta-information about theorem deps *)
-val pgml_version_supported = "1.0";
-val pgmlN = "PGML";
fun pgml () = pgmlN mem_string ! print_mode;
-
-(* text output *)
+(* text output: print modes for xsymbol and PGML *)
local
@@ -47,20 +80,34 @@
| xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
fun xsymbols_output s =
- if Symbol.chars_only s then Symbol.default_output s
- else if Output.has_mode xsymbolsN then
+ if xsymbolsN mem_string ! print_mode 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.symbol_output s;
+ else Symbol.default_output s;
+
+fun pgml_sym s =
+ (case Symbol.decode s of
+ Symbol.Char "\\" => "\\\\"
+ | Symbol.Char s => XML.text s
+ | Symbol.Sym s => XML.element "sym" [("name", s)] []
+ | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []
+ | Symbol.Raw s => s);
-fun pgml_output (s, len) =
- if pgml () then (XML.text s, len)
- else (s, len);
+fun pgml_output str =
+ let val syms = Symbol.explode str
+ in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
+
+in
-in
+fun setup_xsymbols_output () =
+ Output.add_mode
+ xsymbolsN
+ (xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
-fun setup_xsymbols_output () = Output.add_mode proof_generalN
- (pgml_output o xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
+fun setup_pgml_output () =
+ Output.add_mode
+ pgmlN
+ (pgml_output, Symbol.default_indent, Symbol.encode_raw);
end;
@@ -81,8 +128,10 @@
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
fun tagit (kind, bg_tag) x =
- (if pgml () then xml_atom kind x else bg_tag ^ x ^ end_tag,
- real (Symbol.length (Symbol.explode x)));
+ (if Output.has_mode pgmlatomsN then
+ xml_atom kind x
+ else bg_tag ^ x ^ end_tag,
+ real (Symbol.length (Symbol.explode x)));
fun free_or_skolem x =
(case try Syntax.dest_skolem x of
@@ -109,259 +158,184 @@
in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
-(* messages and notification *)
+(* assembling PGIP packets *)
+
+val pgip_refseq = ref None : string option ref
+val pgip_refid = ref None : string option ref
local
+ val myseq_no = ref 1; (* PGIP packet counter *)
-fun decorated_output bg en prfx =
- writeln_default o enclose bg en o prefix_lines prfx;
+ val pgip_class = "pg"
+ val pgip_origin = "Isabelle/Isar"
+ val pgip_id = (getenv "HOSTNAME") ^ "/" ^ (getenv "USER") ^ "/" ^
+ (Time.toString(Time.now()))
+ (* FIXME: PPID is empty for me: any way to get process ID? *)
-fun message kind bg en prfx s =
- if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s])
- else decorated_output bg en prfx s;
-
+ fun assemble_pgips pgips =
+ XML.element
+ "pgip"
+ ([("class", pgip_class),
+ ("origin", pgip_origin),
+ ("id", pgip_id)] @
+ (if_none (apsome (single o (pair "refseq")) (!pgip_refseq)) []) @
+ (if_none (apsome (single o (pair "refid")) (!pgip_refid)) []) @
+ [("seq", string_of_int (Library.inc myseq_no))])
+ pgips
in
-val notify = message "notify" (oct_char "360") (oct_char "361") "";
+ fun decorated_output bg en prfx =
+ writeln_default o enclose bg en o prefix_lines prfx;
+
+ (* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
+ for PG 4.0 which processes PGIP without needing special chars. *)
+ fun issue_pgips ps =
+ if pgip_emacs_compatibility() then
+ decorated_output (* add urgent message annotation *)
+ (oct_char "360") (oct_char "361") ""
+ (assemble_pgips ps)
+ else
+ writeln_default (assemble_pgips ps)
+
+ fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]]
+
+ fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []]
+
+ fun issue_pgip resp attrs = writeln_default o (assemble_pgip resp attrs)
+
+(* FIXME: temporarily to support PG 3.4. *)
+ fun issue_pgip_maybe_decorated bg en resp attrs s =
+ if pgip_emacs_compatibility() then
+ (* in PGIP mode, but using escape characters as well. *)
+ writeln_default (enclose bg en (assemble_pgip resp attrs s))
+ else
+ issue_pgip resp attrs s
+
+ fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs)
+
+end
+
+(* messages and notification *)
+
+fun message resp attrs bg en prfx s =
+ if pgip() then
+ issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s)
+ else
+ decorated_output bg en prfx s;
+
+
+local
+ val display_area = ("area", "display")
+ val message_area = ("area", "message")
+ val tracing_category = ("category", "tracing")
+ val urgent_indication = ("urgent", "y")
+ val nonfatal = ("fatality", "nonfatal")
+ val fatal = ("fatality", "fatal")
+ val panic = ("fatality", "panic")
+
+ val thyname_attr = pair "thyname"
+ val url_attr = pair "url"
+ fun localfile_url_attr path = url_attr ("file:///" ^ path)
+in
fun setup_messages () =
- (writeln_fn := message "output" "" "" "";
- priority_fn := message "information" (oct_char "360") (oct_char "361") "";
- tracing_fn := message "tracing" (oct_char "360" ^ oct_char "375") (oct_char "361") "";
- warning_fn := message "warning" (oct_char "362") (oct_char "363") "### ";
- error_fn := message "error" (oct_char "364") (oct_char "365") "*** ");
+ (writeln_fn := message "normalresponse" [message_area] "" "" "";
+
+ priority_fn := message "normalresponse" [message_area, urgent_indication]
+ (oct_char "360") (oct_char "361") "";
+
+ tracing_fn := message "normalresponse" [message_area, tracing_category]
+ (oct_char "360" ^ oct_char "375") (oct_char "361") "";
+
+ warning_fn := message "errorresponse" [nonfatal]
+ (oct_char "362") (oct_char "363") "### ";
+
+ error_fn := message "errorresponse" [fatal]
+ (oct_char "364") (oct_char "365") "*** ";
+
+ panic_fn := message "errorresponse" [panic]
+ (oct_char "364") (oct_char "365") "!!! ")
+
+
+(* accumulate printed output in a single PGIP response *)
+
+fun with_displaywrap (elt,attrs) dispfn =
+ let
+ val lines = ref ([] : string list);
+ fun wlgrablines s = (lines:= (s :: (!lines)))
+ in
+ (setmp writeln_fn wlgrablines dispfn ();
+ (* FIXME: cat_lines here inefficient, should use stream output *)
+ issue_pgip elt attrs (cat_lines (!lines)))
+ end
-fun tell_clear_goals () = notify "Proof General, please clear the goals buffer.";
-fun tell_clear_response () = notify "Proof General, please clear the response buffer.";
-fun tell_file msg path = notify ("Proof General, " ^ msg ^ " " ^ quote (File.sysify_path path));
-val tell_unlock = tell_file "you can unlock the file";
+val emacs_notify = decorated_output (oct_char "360") (oct_char "361") "";
+
+fun tell_clear_goals () =
+ if pgip() then
+ issue_pgipe "cleardisplay" [display_area]
+ else
+ emacs_notify "Proof General, please clear the goals buffer.";
+
+fun tell_clear_response () =
+ if pgip() then
+ issue_pgipe "cleardisplay" [message_area]
+ else
+ emacs_notify "Proof General, please clear the response buffer.";
-end;
+fun tell_file_loaded path =
+ if pgip() then
+ issue_pgipe "informtheoryloaded" (* FIXME: get thy name from info here? *)
+ [thyname_attr (XML.text (File.sysify_path path)),
+ localfile_url_attr (XML.text (File.sysify_path path))]
+ else
+ emacs_notify ("Proof General, this file is loaded: "
+ ^ quote (File.sysify_path path));
+
+fun tell_file_retracted path =
+ if pgip() then
+ issue_pgipe "informtheoryretracted" (* FIXME: get thy name from info here? *)
+ [thyname_attr (XML.text (File.sysify_path path)),
+ localfile_url_attr (XML.text (File.sysify_path path))]
+ else
+ emacs_notify ("Proof General, you can unlock the file "
+ ^ quote (File.sysify_path path));
(* theory / proof state output *)
local
-fun tmp_markers f =
- setmp Display.current_goals_markers (oct_char "366", oct_char "367", "") f ();
-
-fun statedisplay prts =
- writeln_default (XML.element "statedisplay" [] [Pretty.string_of (Pretty.chunks prts)]);
-
-fun print_current_goals n m st =
- if pgml () then statedisplay (Display.pretty_current_goals n m st)
- else tmp_markers (fn () => Display.print_current_goals_default n m st);
-
-fun print_state b st =
- if pgml () then statedisplay (Toplevel.pretty_state b st)
- else tmp_markers (fn () => Toplevel.print_state_default b st);
-
-in
-
-fun setup_state () =
- (Display.print_current_goals_fn := print_current_goals;
- Toplevel.print_state_fn := print_state;
- Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
+ fun tmp_markers f = setmp Display.current_goals_markers
+ (oct_char "366", oct_char "367", "") f ()
-end;
-
-
-(* theorem dependency output *)
-
-local
-
-val spaces_quote = space_implode " " o map quote;
+ fun statedisplay prts =
+ issue_pgip "proofstate" []
+ (XML.element "pgml" []
+ [XML.element "statedisplay"
+ []
+ [Output.output (* FIXME: needed? *)
+ (Pretty.output
+ (Pretty.chunks prts))]])
-fun tell_thm_deps ths =
- conditional (thm_depsN mem_string ! print_mode) (fn () =>
- let
- val names = map Thm.name_of_thm ths \ "";
- val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
- (Symtab.empty, map Thm.proof_of ths)) \ "";
- in
- if null names orelse null deps then ()
- else notify ("Proof General, theorem dependencies of " ^ spaces_quote names ^ " are "
- ^ spaces_quote deps)
- end);
-
+ fun print_current_goals n m st =
+ if pgml () then statedisplay (Display.pretty_current_goals n m st)
+ else tmp_markers (fn () => Display.print_current_goals_default n m st)
+
+ fun print_state b st =
+ if pgml () then statedisplay (Toplevel.pretty_state b st)
+ else tmp_markers (fn () => Toplevel.print_state_default b st)
in
-fun setup_present_hook () =
- Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
-
-end;
-
-
-(* theory loader actions *)
-
-local
-
-fun add_master_files name files =
- let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
- in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
-
-fun trace_action action name =
- if action = ThyInfo.Update then
- seq (tell_file "this file is loaded:") (ThyInfo.loaded_files name)
- else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
- seq tell_unlock (add_master_files name (ThyInfo.loaded_files name))
- else ();
-
-in
- fun setup_thy_loader () = ThyInfo.add_hook trace_action;
- fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
-end;
-
-
-(* prepare theory context *)
-
-val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
-val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
-
-fun which_context () =
- (case Context.get_context () of
- Some thy => " Using current (dynamic!) one: " ^
- (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
- | None => "");
-
-fun try_update_thy_only file =
- ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
- let val name = thy_name file in
- if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) then update_thy_only name
- else warning ("Unkown theory context of ML file." ^ which_context ())
- end) ();
-
-
-(* get informed about files *)
-
-val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
-val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
-
-fun proper_inform_file_processed file state =
- let val name = thy_name file in
- if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
- (ThyInfo.touch_child_thys name;
- transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
- (warning msg; warning ("Failed to register theory: " ^ quote name);
- tell_unlock (Path.base (Path.unpack file))))
- else raise Toplevel.UNDEF
- end;
-
-fun vacuous_inform_file_processed file state =
- (warning ("No theory " ^ quote (thy_name file));
- tell_unlock (Path.base (Path.unpack file)));
-
-
-(* options *)
-
-fun nat_option r = ("nat",
- (fn () => string_of_int (!r)),
- (fn s => (case Syntax.read_nat s of
- None => error "nat_option: illegal value"
- | Some i => r := i)));
-
-fun bool_option r = ("boolean",
- (fn () => Bool.toString (!r)),
- (fn "false" => r := false | "true" => r := true
- | _ => error "bool_option: illegal value"));
-
-val proof_option = ("boolean",
- (fn () => Bool.toString (!proofs >= 2)),
- (fn "false" => proofs := 1 | "true" => proofs := 2
- | _ => error "proof_option: illegal value"));
+ fun setup_state () =
+ (Display.print_current_goals_fn := print_current_goals;
+ Toplevel.print_state_fn := print_state;
+ (* FIXME: check next octal char won't appear in pgip? *)
+ Toplevel.prompt_state_fn := (suffix (oct_char "372") o
+ Toplevel.prompt_state_default));
+end
-val thm_deps_option = ("boolean",
- (fn () => Bool.toString ("thm_deps" mem !print_mode)),
- (fn "false" => print_mode := Library.gen_rems (op =) (!print_mode, ["thm_deps"])
- | "true" => print_mode := (["thm_deps"] @ !print_mode)
- | _ => error "thm_deps_option: illegal value"));
-
-val print_depth_option = ("nat",
- (fn () => "10"),
- (fn s => (case Syntax.read_nat s of
- None => error "print_depth_option: illegal value"
- | Some i => print_depth i)));
-
-val options = ref
- [("show-types", ("Whether to show types in Isabelle.",
- bool_option show_types)),
- ("show-sorts", ("Whether to show sorts in Isabelle.",
- bool_option show_sorts)),
- ("show-structs", ("Whether to show implicit structures in Isabelle.",
- bool_option show_structs)),
- ("show-consts", ("Whether to show types of consts in Isabelle goals.",
- bool_option show_consts)),
- ("long-names", ("Whether to show fully qualified names in Isabelle.",
- bool_option long_names)),
- ("show-brackets", ("Whether to show full bracketing in Isabelle.",
- bool_option show_brackets)),
- ("eta-contract", ("Whether to print terms eta-contracted in Isabelle.",
- bool_option Syntax.eta_contract)),
- ("trace-simplifier", ("Whether to trace the Simplifier in Isabelle.",
- bool_option trace_simp)),
- ("trace-rules", ("Whether to trace the standard rules in Isabelle.",
- bool_option trace_rules)),
- ("quick-and-dirty", ("Whether to take a few short cuts occasionally.",
- bool_option quick_and_dirty)),
- ("full-proofs", ("Whether to record full proof objects internally.",
- proof_option)),
- ("trace-unification", ("Whether to output error diagnostics during unification.",
- bool_option Pattern.trace_unify_fail)),
- ("show-main-goal", ("Whether to show main goal.",
- bool_option Proof.show_main_goal)),
- ("global-timing", ("Whether to enable timing in Isabelle.",
- bool_option Output.timing)),
- ("theorem-dependencies", ("Whether to track theorem dependencies within Proof General.",
- thm_deps_option)),
- ("goals-limit", ("Setting for maximum number of goals printed in Isabelle.",
- nat_option goals_limit)),
- ("prems-limit", ("Setting for maximum number of premises printed in Isabelle/Isar.",
- nat_option ProofContext.prems_limit)),
- ("print-depth", ("Setting for the ML print depth in Isabelle.",
- print_depth_option))];
-
-
-(* sending PGIP commands to the interface *)
-
-fun issue_pgip pgips = notify (XML.element "pgip" [] pgips);
-
-fun usespgml () =
- issue_pgip [XML.element "usespgml" [("version", pgml_version_supported)] []];
-
-(*NB: the default returned here is actually the current value, so
- repeated uses of <askprefs> will not work correctly*)
-fun show_options () = issue_pgip (map
- (fn (name, (descr, (ty, get, _))) => (XML.element "oldhaspref"
- [("type", ty), ("descr", descr), ("default", get ())] [name])) (!options));
-
-fun set_option name value = (case assoc (!options, name) of
- None => warning ("Unknown option: " ^ quote name)
- | Some (_, (_, _, set)) => set value);
-
-fun get_option name = (case assoc (!options, name) of
- None => warning ("Unknown option: " ^ quote name)
- | Some (_, (_, get, _)) =>
- issue_pgip [XML.element "prefval" [("name", name)] [get ()]]);
-
-
-(* processing PGIP commands from the interface *)
-
-(*FIXME: matching on attributes is a bit too strict here*)
-
-fun process_pgip_element pgip = (case pgip of
- XML.Elem ("askpgml", _, []) => usespgml ()
- | XML.Elem ("askprefs", _, []) => show_options ()
- | XML.Elem ("getpref", [("name", name)], []) => get_option name
- | XML.Elem ("setpref", [("name", name)], [XML.Text value]) =>
- set_option name value
- | XML.Elem (e, _, _) => warning ("Unrecognized PGIP command: " ^ e)
- | XML.Text t => warning ("Unrecognized PGIP command:\n" ^ t));
-
-fun process_pgip s = (case XML.tree_of_string s of
- XML.Elem ("pgip", _, pgips) => seq process_pgip_element pgips
- | _ => warning ("Invalid PGIP packet received\n" ^ s));
-
+end
(* misc commands for ProofGeneral/isa *)
@@ -381,6 +355,70 @@
| repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
+(* theory loader actions *)
+
+local
+
+fun add_master_files name files =
+ let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
+ in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
+
+fun trace_action action name =
+ if action = ThyInfo.Update then
+ seq tell_file_loaded (ThyInfo.loaded_files name)
+ else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
+ seq tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
+ else ();
+
+in
+ fun setup_thy_loader () = ThyInfo.add_hook trace_action;
+ fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
+end;
+
+
+(* prepare theory context *)
+
+val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
+val update_thy_only = setmp MetaSimplifier.trace_simp
+ false ThyInfo.update_thy_only;
+
+fun which_context () =
+ (case Context.get_context () of
+ Some thy => " Using current (dynamic!) one: " ^
+ (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
+ | None => "");
+
+fun try_update_thy_only file =
+ ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
+ let val name = thy_name file in
+ if is_some (ThyLoad.check_file (ThyLoad.thy_path name))
+ then update_thy_only name
+ else warning ("Unkown theory context of ML file." ^ which_context ())
+ end) ();
+
+
+(* get informed about files *)
+
+val inform_file_retracted =
+ ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
+val inform_file_processed =
+ ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
+
+fun proper_inform_file_processed file state =
+ let val name = thy_name file in
+ if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
+ (ThyInfo.touch_child_thys name;
+ transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
+ (warning msg; warning ("Failed to register theory: " ^ quote name);
+ tell_file_retracted (Path.base (Path.unpack file))))
+ else raise Toplevel.UNDEF
+ end;
+
+fun vacuous_inform_file_processed file state =
+ (warning ("No theory " ^ quote (thy_name file));
+ tell_file_retracted (Path.base (Path.unpack file)));
+
+
(* restart top-level loop (keeps most state information) *)
local
@@ -397,16 +435,649 @@
end;
-
fun full_proofs true = proofs := 2
| full_proofs false = proofs := 1;
-(* outer syntax *)
+(* theorem dependency output *)
+
+local
+
+val spaces_quote = space_implode " " o map quote;
+
+fun thm_deps_message (thms, deps) =
+ if pgip() then
+ issue_pgips
+ [XML.element
+ "metainforesponse" (* FIXME: get thy name from info here? *)
+ [("infotype", "isabelle_theorem_dependencies")]
+ [XML.element "value" [("name", "thms")] [XML.text thms],
+ XML.element "value" [("name", "deps")] [XML.text deps]]]
+ else emacs_notify
+ ("Proof General, theorem dependencies of "
+ ^ thms ^ " are " ^ deps)
+
+
+fun tell_thm_deps ths =
+ conditional (thm_depsN mem_string ! print_mode) (fn () =>
+ let
+ val names = map Thm.name_of_thm ths \ "";
+ val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
+ (Symtab.empty, map Thm.proof_of ths)) \ "";
+ in
+ if null names orelse null deps then ()
+ else thm_deps_message (spaces_quote names, spaces_quote deps)
+ end);
+
+in
+
+fun setup_present_hook () =
+ Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
+
+end;
+
+
+(*** Preferences ***)
+
+local
+val pgipnat = XML.element "pgipint" [("min", "0")] []
+fun pgipnatmax max = XML.element "pgipint" [("min", "0"),
+ ("max", string_of_int max)] []
+val pgipbool = XML.element "pgipbool" [] []
+
+fun withdefault f = (f(), f)
+in
+
+fun nat_option r = (pgipnat,
+ withdefault (fn () => string_of_int (!r)),
+ (fn s => (case Syntax.read_nat s of
+ None => error "nat_option: illegal value"
+ | Some i => r := i)));
+
+fun bool_option r = (pgipbool,
+ withdefault (fn () => Bool.toString (!r)),
+ (fn "false" => r := false | "true" => r := true
+ | _ => error "bool_option: illegal value"));
+
+val proof_option = (pgipbool,
+ withdefault (fn () => Bool.toString (!proofs >= 2)),
+ (fn "false" => proofs := 1 | "true" => proofs := 2
+ | _ => error "proof_option: illegal value"));
+
+val thm_deps_option = (pgipbool,
+ withdefault (fn () => Bool.toString (Output.has_mode "thm_deps")),
+ (fn "false" => print_mode := ((!print_mode) \ "thm_deps")
+ | "true" => print_mode := ("thm_deps" ins (!print_mode))
+ | _ => error "thm_deps_option: illegal value"));
+
+local
+ val pg_print_depth_val = ref 10
+ fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
+in
+val print_depth_option = (pgipnat,
+ withdefault (fn () => string_of_int (!pg_print_depth_val)),
+ (fn s => (case Syntax.read_nat s of
+ None => error "print_depth_option: illegal value"
+ | Some i => pg_print_depth i)))
+end
+
+val preferences = ref
+ [("Display",
+ [("show-types",
+ ("Include types in display of Isabelle terms",
+ bool_option show_types)),
+ ("show-sorts",
+ ("Include sorts in display of Isabelle terms",
+ bool_option show_sorts)),
+ ("show-consts",
+ ("Show types of consts in Isabelle goal display",
+ bool_option show_consts)),
+ ("long-names",
+ ("Show fully qualified names in Isabelle terms", bool_option long_names)),
+ ("show-brackets",
+ ("Show full bracketing in Isabelle terms",
+ bool_option show_brackets)),
+ ("show-main-goal",
+ ("Show main goal in proof state display", bool_option Proof.show_main_goal)),
+ ("eta-contract",
+ ("Print terms eta-contracted",
+ bool_option Syntax.eta_contract))]),
+ ("Advanced Display",
+ [("goals-limit",
+ ("Setting for maximum number of goals printed",
+ nat_option goals_limit)),
+ ("prems-limit",
+ ("Setting for maximum number of premises printed",
+ nat_option ProofContext.prems_limit)),
+ ("print-depth",
+ ("Setting for the ML print depth",
+ print_depth_option))]),
+ ("Tracing",
+ [("trace-simplifier",
+ ("Trace simplification rules.",
+ bool_option trace_simp)),
+ ("trace-rules", ("Trace application of the standard rules",
+ bool_option trace_rules)),
+ ("trace-unification",
+ ("Output error diagnostics during unification",
+ bool_option Pattern.trace_unify_fail)),
+ ("global-timing",
+ ("Whether to enable timing in Isabelle.",
+ bool_option Output.timing))]),
+ ("Proof",
+ [("quick-and-dirty",
+ ("Take a few (interactive-only) short cuts",
+ bool_option quick_and_dirty)),
+ ("full-proofs",
+ ("Record full proof objects internally",
+ proof_option)),
+ ("theorem-dependencies",
+ ("Track theorem dependencies within Proof General",
+ thm_deps_option))])
+ ];
+end
+
+(* Configuration: GUI config, proverinfo messages *)
+
+local
+ val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
+ val name_attr = pair "name"
+ val version_attr = pair "version"
+ val isabelle_www = "http://isabelle.in.tum.de/"
+in
+fun send_pgip_config () =
+ let
+ val path = Path.unpack config_file
+ val exists = File.exists path
+ val proverinfo =
+ XML.element "proverinfo"
+ [("name",Session.name()), ("version", version),
+ ("url", isabelle_www)]
+ [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
+ XML.element "helpdoc"
+ (* NB: would be nice to generate/display docs from isatool
+ doc, but that program may not be running on same machine;
+ front end should be responsible for launching viewer, etc. *)
+ [("name", "Isabelle/HOL Tutorial"),
+ ("descr", "A Gentle Introduction to Isabelle/HOL"),
+ ("url", "http://isabelle.in.tum.de/dist/Isabelle2003/doc/tutorial.pdf")]
+ []]
+ in
+ if exists then
+ (issue_pgips [proverinfo]; issue_pgips [File.read path])
+ else panic ("PGIP configuration file " ^ config_file ^ " not found")
+ end;
+end
+
+
+(* PGIP identifier tables (prover objects). [incomplete] *)
+
+local
+ val objtype_thy = "theory"
+ val objtype_thm = "theorem"
+ val objtype_term = "term"
+ val objtype_type = "type"
+
+ fun xml_idtable ty ctx ids =
+ let
+ fun ctx_attr (Some c)= [("context", c)]
+ | ctx_attr None = []
+ fun xmlid x = XML.element "identifier" [] [XML.text x];
+ in
+ XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
+ (map xmlid ids)
+ end
+in
+
+fun setids t = issue_pgip "setids" [] t
+fun addids t = issue_pgip "addids" [] t
+fun delids t = issue_pgip "delids" [] t
+
+fun delallids ty = setids (xml_idtable ty None [])
+
+fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
+fun clear_thy_idtable () = delallids objtype_thy
+
+fun send_thm_idtable ctx thy =
+ addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
+
+fun clear_thm_idtable () = delallids objtype_thm
+
+(* fun send_type_idtable thy = TODO, it's a bit low-level messy
+ & maybe not so useful anyway *)
+
+end
+
+(* Response to interface queries about known objects *)
+
+local
+ val topthy = Toplevel.theory_of o Toplevel.get_state
+ val pthm = print_thm oo get_thm
+
+ fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
+in
+fun askids (None, Some "theory") = send_thy_idtable None (ThyInfo.names())
+ | askids (None, None) = send_thy_idtable None (ThyInfo.names())
+ (* only theories known in top context *)
+ | askids (Some thy, Some "theory") = send_thy_idtable (Some thy) (ThyInfo.get_preds thy)
+ | askids (Some thy, Some "theorem") = send_thm_idtable (Some thy) (ThyInfo.get_theory thy)
+ | askids (Some thy, None) = (send_thy_idtable (Some thy) (ThyInfo.get_preds thy);
+ send_thm_idtable (Some thy) (ThyInfo.get_theory thy))
+(* | askids (Some thy, "type") = send_type_idtable (Some thy) (ThyInfo.get_theory thy) *)
+ | askids (_, Nothing) = error "No objects of any type are available here."
+ | askids (_, Some ot) = error ("No objects of type "^(quote ot)^" are available here.")
+
+fun showid (_, "theory", n) =
+ with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
+ | showid (Some thy, "theorem", t) =
+ with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
+ | showid (None, "theorem", t) =
+ with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
+ | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
+
+(* Return script command to set an identifier to some value *)
+(* TODO: support object preference setting here *)
+fun bindid (name, "thm", [XML.Elem ("objval",_,[XML.Text objval])]) =
+ ("lemmas " ^ name ^ " = " ^ objval)
+ | bindid (name, ot, _) = error ("Cannot bind objects of type " ^ ot)
+
+end
+
+(** Parsing proof scripts without execution **)
+
+local
+ (* This is a temporary hack until we have decent parsing of proof scripts *)
+ fun xmle elt = XML.element elt [] []
+ fun xmlc elt str = XML.element elt [] [XML.text str]
+
+ fun make_opengoal args =
+ (* For now, strictly only args like <lemma foo: "P->Q"> *)
+ let
+ val tstart = find_index_eq "\"" (explode args)
+ val tend = find_index_eq "\"" (drop (tstart, (explode args)))
+ val nend = find_index_eq ":" (explode args)
+ val uptonend = (rev (take (nend-1,explode args)))
+ val nstart = (length uptonend) -
+ (find_index (not o Symbol.is_letter) uptonend)
+ in
+ (XML.element
+ "opengoal"
+ [("thmname", String.substring(args,nstart,nend-nstart))]
+ [XML.text (String.substring(args, tstart+1, tend))])
+ end
+
+ fun make_theory args =
+ (* For now, strictly only args like <theory Foo=Main:> *)
+ let
+ val argstart = find_index_eq "=" (explode args)
+ val argend = find_index_eq ":" (explode args)
+ val (name1,arg1) = splitAt(argstart, explode args)
+ val namecs = dropwhile (fn c => c mem [" ","\t","\n"]) (rev name1)
+ val nameend = find_index (fn c=> not (Symbol.is_quasi_letter c)) namecs
+ val (namecs',_) = splitAt(nameend, namecs)
+ val name = implode (rev namecs')
+ val (arg2, _) = splitAt(argend-argstart-1, tl arg1)
+ val arg = implode arg2
+ in
+ XML.element "opentheory" [("thyname", name)] [XML.text arg]
+ end
+in
+fun xmls_of_transition (name,toks,tr) =
+ let
+ val str = name ^ " " ^ (space_implode " " (map OuterLex.unparse toks))
+ in
+ case name of (* NB: see isar_syn.ML for names of standard commands *)
+ "done" => [xmle "closegoal"]
+ | "sorry" => [xmle "giveupgoal"]
+ | "oops" => [xmle "postponegoal"]
+ | "by" => [xmlc "proofstep" ("apply " ^ str),
+ xmle "closegoal"] (* FIXME: tactic proofs only just now *)
+ (* theories *)
+ | "theory" => [make_theory str]
+ (* goals *)
+ | "lemma" => [make_opengoal str]
+ | "theorem" => [make_opengoal str]
+ | "corollary" => [make_opengoal str]
+ (* literate text *)
+ | "text" => [xmlc "litcomment" str]
+ | "sect" => [xmlc "litcomment" ("ion " ^ str)]
+ | "subsect" => [xmlc "litcomment" ("ion " ^ str)]
+ | "subsubsect" => [xmlc "litcomment" ("ion " ^ str)]
+ | "txt" => [xmlc "litcomment" str]
+ | _ => [xmlc "proofstep" str] (* default for anything else *)
+ end
+
+(* FIXME: need to handle parse errors gracefully below, perhaps returning partial parse *)
+(* NB: comments are ignored by below; not good if we use this to reconstruct script *)
+
+fun xmls_of_str str =
+ let fun parse_loop (nm_lex_trs,xmls) =
+ (case nm_lex_trs of
+ [] => xmls
+ | (nm,toks,tr)::rest =>
+ let
+ val xmls_tr = xmls_of_transition (nm,toks,tr)
+ in
+ parse_loop (rest, xmls @ xmls_tr)
+ end)
+ in
+ parse_loop (OuterSyntax.read str, [])
+ end
+
+
+fun parsescript str =
+ issue_pgips [XML.element "parseresult" [] (xmls_of_str str)]
+
+end
+
+
+
+(**** PGIP: Isabelle -> Interface ****)
+
+val isabelle_pgml_version_supported = "1.0";
+val isabelle_pgip_version_supported = "1.0"
+
+fun usespgip () =
+ issue_pgipe "usespgip" [("version", isabelle_pgip_version_supported)];
+
+fun usespgml () =
+ issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)];
+
+fun hasprefs () =
+ seq (fn (prefcat, prefs) =>
+ issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
+ (map (fn (name, (descr, (ty, (default,_),_))) =>
+ XML.element "haspref" [("name", name),
+ ("descr", descr),
+ ("default", default)]
+ [ty]) prefs)]) (!preferences);
+
+fun allprefs () = foldl (op @) ([], map snd (!preferences))
+
+fun setpref name value =
+ (case assoc (allprefs(), name) of
+ None => warning ("Unknown pref: " ^ quote name)
+ | Some (_, (_, _, set)) => set value);
+
+fun getpref name =
+ (case assoc (allprefs(), name) of
+ None => warning ("Unknown pref: " ^ quote name)
+ | Some (_, (_, (_,get), _)) =>
+ issue_pgip "prefval" [("name", name)] (get ()));
+
+
+
+
+
+(**** PGIP: Interface -> Isabelle/Isar ****)
+
+exception PGIP of string;
+exception PGIP_QUIT;
+
+(* Sending commands to Isar *)
+
+(* FIXME Makarius:
+ 'isarcmd': consider using 'Toplevel.>>>' instead of
+ 'Toplevel.loop'; unsure about the exact error behaviour required here;
+*)
+val isarcmd = Toplevel.loop o
+ (OuterSyntax.isar_readstring
+ (Position.name "PGIP message")) (* FIXME: could do better *)
+
+fun isarscript s = isarcmd s (* send a script command *)
+ (* was: (isarcmd s; issue_pgip "scriptinsert" [] (XML.text s)) *)
+
+
+(* load an arbitrary (.thy or .ML) file *)
+
+fun use_thy_or_ml_file file =
+ let
+ val (path,extn) = Path.split_ext (Path.unpack file)
+ in
+ case extn of
+ "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
+ | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
+ | "ML" => isarcmd ("use " ^ quote file)
+ (* instead of error we could guess theory? *)
+ | other => error ("Don't know how to read a file with extension " ^ other)
+ end
+
+
+local
+ (* Proof control commands *)
+
+ fun xmlattro attrs attr = assoc(attrs,attr)
+
+ fun xmlattr attrs attr =
+ (case xmlattro attrs attr of
+ Some value => value
+ | None => raise PGIP ("Missing attribute: " ^ attr))
+
+ fun xmltext [XML.Text text] = text
+ | xmltext ((XML.Text text)::ts) = text ^ " " ^ (xmltext ts) (* FIXME: space shouldn't be needed *)
+ | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
+
+ val thyname_attr = "thyname"
+ val objtype_attr = "objtype"
+ val name_attr = "name"
+ val dirname_attr = "dir"
+ fun comment x = "(* " ^ x ^ " *)"
+
+(* return script portion corresponding to a PGIP command.
+ We only unparse proper proof commands.
+ (we might unparse gui opns too, if they didn't have opcmd settings?)
+*)
+ fun unparse (elem,attrs,xmls) =
+ (case elem of
+ "opengoal" => "lemma " ^ (xmlattr attrs "thmname") ^ ": " ^
+ (quote (xmltext xmls))
+ (* FIXME: should maybe remove ^^^^^^^^^^
+ to provide for Isar's parenthetical phrases (is ...) *)
+ | "proofstep" => xmltext xmls
+ | "closegoal" => "done" (* FIXME: or qed? Maybe nothing? *)
+
+ | "opentheory" => ("theory " ^ (xmlattr attrs thyname_attr) ^
+ " = " ^ (xmltext xmls) ^ ":")
+ | "closetheory" => "end"
+ | "postponegoal" => "sorry"
+ | "giveupgoal" => "oops"
+
+ | "bindid" => (bindid (xmlattr attrs objtype_attr,
+ xmlattr attrs name_attr,
+ xmls))
+ | "comment" => comment (xmltext xmls)
+ | "litcomment" => xmltext xmls
+ | _ => error ("unparse called with improper proof command: " ^ elem))
+
+ fun unparsecmds xmls =
+ let
+ fun upc (XML.Elem elt) = (unparse elt)
+ | upc (XML.Text t) = (warning ("unprasecmds: ignoring spurious text: " ^ t); "")
+ in
+ issue_pgip "unparseresult" []
+ (XML.text (cat_lines (map upc xmls))) (* FIXME: use cdata? *)
+ end
+
+ (* parse URLs like "file://host/name.thy" *)
+ (* FIXME: instead of this, extend code in General/url.ML & use that. *)
+ fun decode_url url =
+ (let
+ val sep = find_index_eq ":" (explode url)
+ val proto = String.substring(url,0,sep)
+ val hostsep = find_index_eq "/" (drop (sep+3,explode url))
+ val host = String.substring(url,sep+3,hostsep-sep+4)
+ val doc = if (size url >= sep+hostsep+3) then
+ String.substring(url,sep+hostsep+4,size url-hostsep-sep-4)
+ else ""
+ in
+ (proto,host,doc)
+ end) handle Subscript => error ("Badly formed URL " ^ url)
+
+ fun localfile_of_url url =
+ let
+ val (proto,host,name) = decode_url url
+ in
+ if (proto = "file" andalso
+ (host = "" orelse
+ host = "localhost" orelse
+ host = (getenv "HOSTNAME")))
+ then name
+ else error ("Cannot access non-local URL " ^ url)
+ end
+
+ fun fileurl_of attrs = localfile_of_url (xmlattr attrs "url")
+
+ val topthy = Toplevel.theory_of o Toplevel.get_state
+ val topthy_name = PureThy.get_name o topthy
+
+ val currently_open_file = ref (None : string option)
+in
+
+fun process_pgip_element pgipxml =
+ (case pgipxml of
+ (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
+ | (XML.Elem (xml as (elem, attrs, xmls))) => (case elem of
+(* protocol config *)
+ "askpgip" => (usespgip (); send_pgip_config ())
+| "askpgml" => usespgml ()
+(* proverconfig *)
+| "askprefs" => hasprefs ()
+| "getpref" => getpref (xmlattr attrs name_attr)
+| "setpref" => setpref (xmlattr attrs name_attr) (xmltext xmls)
+(* provercontrol *)
+| "proverinit" => isar_restart ()
+| "proverexit" => isarcmd "quit"
+| "startquiet" => isarcmd "disable_pr"
+| "stopquiet" => isarcmd "enable_pr"
+| "pgmlsymbolson" => (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
+| "pgmlsymbolsoff" => (print_mode := (Library.gen_rems
+ (op =) (! print_mode, ["xsymbols", "symbols"])))
+(* provercmd: proper commands which belong in script *)
+| "proofstep" => isarscript (unparse xml)
+| "opengoal" => isarscript (unparse xml)
+| "closegoal" => isarscript (unparse xml)
+| "postponegoal" => isarscript (unparse xml)
+| "giveupgoal" => isarscript (unparse xml)
+| "comment" => isarscript (unparse xml)
+| "litcomment" => isarscript (unparse xml)
+(* provercmd: improper commands which *do not* belong in script *)
+| "undostep" => isarcmd "ProofGeneral.undo"
+| "abortgoal" => isarcmd "ProofGeneral.kill_proof"
+| "forget" => error ("Not implemented")
+| "restoregoal" => error ("Not implemented") (* could just treat as forget? *)
+(* proofctxt: improper commands *)
+| "askids" => askids (xmlattro attrs thyname_attr,
+ xmlattro attrs objtype_attr)
+| "showid" => showid (xmlattro attrs thyname_attr,
+ xmlattr attrs objtype_attr,
+ xmlattr attrs name_attr)
+| "parsescript" => parsescript (xmltext xmls)
+| "unparsecmds" => unparsecmds xmls
+| "showproofstate" => isarcmd "pr"
+| "showctxt" => isarcmd "print_theory" (* more useful than print_context *)
+| "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext xmls))
+| "setlinewidth" => isarcmd ("pretty_setmargin " ^ (xmltext xmls))
+(* proofctxt: proper commands *)
+| "bindid" => isarscript (unparse xml)
+(* filecmd: proper commands *)
+| "opentheory" => isarscript (unparse xml)
+| "closetheory" => (isarscript (unparse xml);
+ writeln ("Theory "^(topthy_name())^" completed."))
+(* filecmd: improper commands *)
+| "aborttheory" => isarcmd ("init_toplevel")
+| "retracttheory" => isarcmd ("kill_thy " ^
+ (quote (xmlattr attrs thyname_attr)))
+| "loadfile" => use_thy_or_ml_file (fileurl_of attrs)
+| "openfile" => (inform_file_retracted (fileurl_of attrs);
+ currently_open_file := Some (fileurl_of attrs))
+| "closefile" => (case !currently_open_file of
+ Some f => (inform_file_processed f;
+ currently_open_file := None)
+ | None => raise PGIP ("closefile when no file is open!"))
+| "abortfile" => (currently_open_file := None) (* might give error for no file open *)
+| "changecwd" => ThyLoad.add_path (xmlattr attrs dirname_attr)
+(* unofficial command for debugging *)
+| "quitpgip" => raise PGIP_QUIT
+| _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
+
+fun process_pgip_tree s =
+ (pgip_refseq := None;
+ pgip_refid := None;
+ (case s of
+ XML.Elem ("pgip", attrs, pgips) =>
+ (let
+ val class = xmlattr attrs "class"
+ val _ = (pgip_refseq := xmlattro attrs "seq";
+ pgip_refid := xmlattro attrs "id")
+ in
+ if (class = "pa") then
+ seq process_pgip_element pgips
+ else
+ raise PGIP "PGIP packet for me should have class=\"pa\""
+ end)
+ | _ => raise PGIP "Invalid PGIP packet received")
+ handle (PGIP msg) =>
+ (error (msg ^ "\nPGIP error occured in XML text below:\n" ^
+ (XML.string_of_tree s))))
+
+(* for export to Emacs *)
+(* val process_pgip = process_pgip_tree o XML.tree_of_string; *)
+(* FIXME: for temporary compatibility with PG 3.4, we engage special characters
+ during output *)
+fun process_pgip s =
+ (pgip_emacs_compatibility_flag := true;
+ process_pgip_tree (XML.tree_of_string s);
+ pgip_emacs_compatibility_flag := false)
+end
+
+
+
+
+(* PGIP loop: process PGIP input only *)
+
+local
+(* NB: simple tty for now; later might read from other sources, open sockets, etc. *)
+(* FIXME da: doesn't setting the stopper at a single element mean we have to
+ parse the whole tree on one go anyway? *)
+val tty_src = Source.set_prompt ""
+ (Source.source Symbol.stopper (XML.parse_elem >> single)
+ None Source.tty);
+
+(* FIXME: Makarius:
+ 'read_pgip()': some content may be left in the internal buffer after
+ Source.get_single, which will got lost between calls; try to avoid
+ building the tty source over and over again;
+*)
+
+fun read_pgip () = Source.get_single tty_src
+
+fun loop () =
+ let
+ val _ = issue_pgipe "ready" []
+ in
+ case (read_pgip()) of
+ None => ()
+ | Some (pgip,_) => (process_pgip_tree pgip; loop()) handle e => handler e
+ end handle e => handler e
+
+and handler e =
+ case e of
+ PGIP_QUIT => ()
+ | ERROR => loop() (* message already given *)
+ | Interrupt => (error "Interrupt during PGIP processing"; loop())
+ | Toplevel.UNDEF => (error "No working context defined"; loop()) (* usually *)
+ | e => (error (Toplevel.exn_message e); loop())
+ (* Also seen: Scan.FAIL (not exported from Scan -- needs catching in xml.ML) *)
+in
+ val pgip_toplevel = loop
+end
+
+
+(* additional outer syntax for Isar *)
local structure P = OuterParse and K = OuterSyntax.Keyword in
-val undoP =
+val undoP = (* undo without output *)
OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
(Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
@@ -455,10 +1126,16 @@
val initialized = ref false;
-fun init isar =
+fun set_prompts true _ = ml_prompts "ML> " "ML# "
+ | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
+ | set_prompts false false =
+ ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
+
+fun init_setup isar pgip =
(conditional (not (! initialized)) (fn () =>
(if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
setup_xsymbols_output ();
+ setup_pgml_output ();
setup_messages ();
setup_state ();
setup_thy_loader ();
@@ -466,27 +1143,43 @@
set initialized; ()));
sync_thy_loader ();
print_mode := proof_generalN :: (! print_mode \ proof_generalN);
+ if pgip then
+ print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN))
+ else ();
set quick_and_dirty;
ThmDeps.enable ();
- if isar then ml_prompts "ML> " "ML# "
- else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
- if isar then (welcome (); Isar.sync_main ()) else isa_restart ());
+ set_prompts isar pgip;
+ pgip_active := pgip)
+
+fun init isar =
+ (init_setup isar false;
+ if isar then ((* da: this welcome is problematic: clashes with welcome
+ issued for PG anyway.
+ welcome (); *)
+ Isar.sync_main ()) else isa_restart ());
+
+fun init_pgip false = panic "Sorry, PGIP not supported for Isabelle/classic mode."
+ | init_pgip true = (init_setup true true; pgip_toplevel());
-(** generate keyword classification file **)
+(** generate keyword classification elisp file **)
local
val regexp_meta = explode ".*+?[]^$";
-val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
+val regexp_quote =
+ implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c)
+ o explode;
fun defconst name strs =
"\n(defconst isar-keywords-" ^ name ^
"\n '(" ^ space_implode "\n " (map (quote o regexp_quote) strs) ^ "))\n";
fun make_elisp_commands commands kind =
- defconst kind (mapfilter (fn (c, _, k, _) => if k = kind then Some c else None) commands);
+ defconst kind (mapfilter
+ (fn (c, _, k, _) => if k = kind then Some c else None)
+ commands);
fun make_elisp_syntax (keywords, commands) =
";;\n\
@@ -496,7 +1189,7 @@
\;; $" ^ "Id$\n\
\;;\n" ^
defconst "major" (map #1 commands) ^
- defconst "minor" (filter Syntax.is_ascii_identifier keywords) ^
+ defconst "minor" (filter Syntax.is_identifier keywords) ^
implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
"\n(provide 'isar-keywords)\n";
@@ -505,8 +1198,9 @@
fun write_keywords s =
(init_outer_syntax ();
File.write (Path.unpack ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
- (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
+ (make_elisp_syntax (OuterSyntax.dest_keywords (),
+ OuterSyntax.dest_parsers ())));
end;
-end;
+end