--- a/src/Pure/proof_general.ML Fri Dec 29 18:46:06 2006 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1525 +0,0 @@
-(* Title: Pure/proof_general.ML
- ID: $Id$
- Author: David Aspinall and Markus Wenzel
-
-Isabelle configuration for Proof General (see
-http://proofgeneral.inf.ed.ac.uk). Also includes experimental support
-for PGIP control language for Isabelle/Isar (PGIP 2.X).
-*)
-
-signature PROOF_GENERAL =
-sig
- val update_thy_only: string -> unit
- val try_update_thy_only: string -> unit
- val inform_file_retracted: string -> unit
- val inform_file_processed: string -> unit
- 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
- val show_context: unit -> theory
- val kill_goal: unit -> unit
- 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
- val xmls_of_str: string -> string list (*temp for testing parser*)
-end;
-
-structure ProofGeneral: PROOF_GENERAL =
-struct
-
-structure P = OuterParse;
-
-
-(* 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"; (*token markup (colouring vars, etc.)*)
-val pgasciiN = "PGASCII"; (*plain 7-bit ASCII communication*)
-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*)
-
-fun pgml () = Output.has_mode pgmlN;
-
-fun special oct =
- if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
- else oct_char oct;
-
-
-(* text output: print modes for xsymbol and PGML *)
-
-local
-
-fun xsym_output "\\" = "\\\\"
- | 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
- let val syms = Symbol.explode s
- in (implode (map xsym_output syms), real (Symbol.length syms)) end
- else Symbol.default_output s;
-
-fun pgml_sym s =
- (case Symbol.decode s of
- (*NB: an alternative here would be to output the default print mode alternative
- in the element content, but unfortunately print modes are not that fine grained.*)
- Symbol.Char s => XML.text s
- | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
- | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
- | Symbol.Raw s => s);
-
-fun pgml_output str =
- let val syms = Symbol.explode str
- in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
-
-in
-
-fun setup_xsymbols_output () =
- Output.add_mode Symbol.xsymbolsN
- (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
-
-fun setup_pgml_output () =
- Output.add_mode pgmlN
- (pgml_output, K pgml_output, Symbol.default_indent, Symbol.encode_raw);
-
-end;
-
-
-(* token translations *)
-
-local
-
-fun end_tag () = special "350";
-val class_tag = ("class", fn () => special "351");
-val tfree_tag = ("tfree", fn () => special "352");
-val tvar_tag = ("tvar", fn () => special "353");
-val free_tag = ("free", fn () => special "354");
-val bound_tag = ("bound", fn () => special "355");
-val var_tag = ("var", fn () => special "356");
-val skolem_tag = ("skolem", fn () => special "357");
-
-fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
-
-fun tagit (kind, bg_tag) 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 Name.dest_skolem x of
- NONE => tagit free_tag x
- | SOME x' => tagit skolem_tag x');
-
-fun var_or_skolem s =
- (case Syntax.read_variable s of
- SOME (x, i) =>
- (case try Name.dest_skolem x of
- NONE => tagit var_tag s
- | SOME x' => tagit skolem_tag
- (setmp show_question_marks true Syntax.string_of_vname (x', i)))
- | NONE => tagit var_tag s);
-
-val proof_general_trans =
- Syntax.tokentrans_mode proof_generalN
- [("class", tagit class_tag),
- ("tfree", tagit tfree_tag),
- ("tvar", tagit tvar_tag),
- ("free", free_or_skolem),
- ("bound", tagit bound_tag),
- ("var", var_or_skolem)];
-
-in
-
-val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
-
-end;
-
-
-(* assembling PGIP packets *)
-
-val pgip_refid = ref NONE: string option ref;
-val pgip_refseq = ref NONE: string option ref;
-
-local
- val pgip_class = "pg"
- val pgip_tag = "Isabelle/Isar"
- val pgip_id = ref ""
- val pgip_seq = ref 0
- fun pgip_serial () = inc pgip_seq
-
- fun assemble_pgips pgips =
- XML.element
- "pgip"
- ([("tag", pgip_tag),
- ("class", pgip_class),
- ("seq", string_of_int (pgip_serial())),
- ("id", !pgip_id)] @
- the_default [] (Option.map (single o (pair "destid")) (! pgip_refid)) @
- (* destid=refid since Isabelle only communicates back to sender,
- so we may omit refid from attributes.
- the_default [] (Option.map (single o (pair "refid")) (! pgip_refid)) @
- *)
- the_default [] (Option.map (single o (pair "refseq")) (! pgip_refseq)))
- pgips;
-
-in
-
-fun init_pgip_session_id () =
- pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
- getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
-
-
-fun matching_pgip_id id = (id = !pgip_id)
-
-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*)
- (special "360") (special "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 []];
-
-(* FIXME: need to add stuff to gather PGIPs here *)
-fun issue_pgip resp attrs txt =
- if pgip_emacs_compatibility () then
- decorated_output (*add urgent message annotation*)
- (special "360") (special "361") ""
- (assemble_pgip resp attrs txt)
- else
- writeln_default (assemble_pgip resp attrs txt);
-
-(* 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 *)
-
-local
- val delay_msgs = ref false; (*true: accumulate messages*)
- val delayed_msgs = ref [];
-in
-
-fun message resp attrs bg en prfx s =
- if pgip () then
- (if (! delay_msgs) then
- delayed_msgs := (resp, attrs, prefix_lines prfx s) :: ! delayed_msgs (*NB: no decs*)
- else
- issue_pgip_maybe_decorated bg en resp attrs
- (XML.element "pgmltext" [] [prefix_lines prfx s]))
- else decorated_output bg en prfx s;
-
-fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []);
-
-fun end_delayed_msgs () = (reset delay_msgs;
- (! delayed_msgs) |> map (fn (resp, attrs, s) =>
- XML.element resp attrs [XML.element "pgmltext" [] [s]]));
-
-end;
-
-local
- val display_area = ("area", "display");
- val message_area = ("area", "message");
- val internal_category = ("messagecategory", "internal");
- val info_category = ("messagecategory", "information");
- val tracing_category = ("messagecategory", "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 abspath = url_attr ("file:" ^ abspath);
-in
-
-fun setup_messages () =
- (writeln_fn := (fn s => message "normalresponse" [message_area] "" "" "" s);
- priority_fn := (fn s => message "normalresponse" [message_area, urgent_indication]
- (special "360") (special "361") "" s);
- tracing_fn := (fn s => message "normalresponse" [message_area, tracing_category]
- (special "360" ^ special "375") (special "361") "" s);
- info_fn := (fn s => message "normalresponse" [message_area, info_category]
- (special "362") (special "363") "+++ " s);
- debug_fn := (fn s => message "normalresponse" [message_area, internal_category]
- (special "362") (special "363") "+++ " s);
- warning_fn := (fn s => message "errorresponse" [nonfatal]
- (special "362") (special "363") "### " s);
- error_fn := (fn s => message "errorresponse" [fatal]
- (special "364") (special "365") "*** " s);
- panic_fn := (fn s => message "errorresponse" [panic]
- (special "364") (special "365") "!!! " s));
-
-
-(* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
-
-fun with_displaywrap (elt, attrs) dispfn =
- let
- val lines = ref ([]: string list);
- fun wlgrablines s = lines := s :: ! lines;
- in
- setmp writeln_fn wlgrablines dispfn ();
- (* IMPORTANT FIXME: XML.element here too inefficient, should use stream output *)
- issue_pgip elt attrs (XML.element "pgmltext" [] (! lines))
- end;
-
-fun emacs_notify s = decorated_output (special "360") (special "361") "" s;
-
-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.";
-
-fun tell_file_loaded path =
- if pgip () then
- issue_pgipe "informfileloaded"
- [localfile_url_attr (XML.text (File.platform_path
- (File.full_path path)))]
- else
- emacs_notify ("Proof General, this file is loaded: " ^
- quote (File.platform_path path));
-
-fun tell_file_retracted path =
- if pgip() then
- issue_pgipe "informfileretracted"
- [localfile_url_attr (XML.text (File.platform_path
- (File.full_path path)))]
- else
- emacs_notify ("Proof General, you can unlock the file "
- ^ quote (File.platform_path path));
-
-
-(* theory / proof state output *)
-
-local
-
-fun tmp_markers f =
- setmp Display.current_goals_markers (special "366", special "367", "") f ();
-
-fun statedisplay prts =
- issue_pgip "proofstate" []
- (XML.element "pgml" []
- [XML.element "statedisplay" [] [Pretty.output (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;
- (* FIXME: check next octal char won't appear in pgip? *)
- Toplevel.prompt_state_fn := (fn s => suffix (special "372")
- (Toplevel.prompt_state_default s)));
-
-end;
-
-end;
-
-
-(* misc commands for ProofGeneral/isa *)
-
-fun thms_containing ss =
- FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE
- (map (fn s => (true, FindTheorems.Pattern s)) ss);
-
-val welcome = priority o Session.welcome;
-val help = welcome;
-val show_context = Context.the_context;
-
-fun kill_goal () = (OldGoals.reset_goals (); tell_clear_goals ());
-
-fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
-
-fun repeat_undo 0 = ()
- | repeat_undo 1 = undo ()
- | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
-
-
-(* theory loader actions *)
-
-local
-
-fun trace_action action name =
- if action = ThyInfo.Update then
- List.app tell_file_loaded (ThyInfo.loaded_files name)
- else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
- List.app tell_file_retracted (ThyInfo.loaded_files name)
- else ();
-
-in
- fun setup_thy_loader () = ThyInfo.add_hook trace_action;
- fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
-end;
-
-
-(* prepare theory context *)
-
-val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
-
-(* FIXME general treatment of tracing*)
-val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
-
-fun dynamic_context () =
- (case Context.get_context () of
- SOME thy => " Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
- | NONE => "");
-
-fun try_update_thy_only file =
- ThyLoad.cond_add_path (Path.dir (Path.explode file)) (fn () =>
- let val name = thy_name file in
- if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name))
- then update_thy_only name
- else warning ("Unkown theory context of ML file." ^ dynamic_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;
-val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) 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;
- ThyInfo.pretend_use_thy_only name handle ERROR msg =>
- (warning msg; warning ("Failed to register theory: " ^ quote name);
- tell_file_retracted (Path.base (Path.explode 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.explode file)));
-
-
-(* restart top-level loop (keeps most state information) *)
-
-local
-
-fun restart isar =
- (if isar then tell_clear_goals () else kill_goal ();
- tell_clear_response ();
- welcome ());
-
-in
-
-fun isa_restart () = restart false;
-fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
-
-end;
-
-fun full_proofs true = proofs := 2
- | full_proofs false = proofs := 1;
-
-
-(* 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);
-
-(* FIXME: check this uses non-transitive closure function here *)
-fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
- let
- val names = filter_out (equal "") (map PureThy.get_name_hint ths);
- val deps = filter_out (equal "")
- (Symtab.keys (fold Proofterm.thms_of_proof
- (map Thm.proof_of ths) Symtab.empty));
- 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 (maps #2 res));
-
-end;
-
-
-
-(** preferences **)
-
-local
-
-fun signed_string_of_int i =
- if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;
-
-val pgipint = XML.element "pgipint" [] [];
-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 with_default f = (f (), f);
-
-in
-
-fun int_option r = (pgipint,
- with_default (fn () => signed_string_of_int (! r)),
- (fn s => (case Syntax.read_int s of
- NONE => error ("int_option: illegal value: " ^ s)
- | SOME i => r := i)));
-
-fun nat_option r = (pgipnat,
- with_default (fn () => string_of_int (! r)),
- (fn s => (case Syntax.read_nat s of
- NONE => error ("nat_option: illegal value: " ^ s)
- | SOME i => r := i)));
-
-fun bool_option r = (pgipbool,
- with_default (fn () => Bool.toString (! r)),
- (fn "false" => r := false | "true" => r := true
- | x => error ("bool_option: illegal value: " ^ x)));
-
-val proof_option = (pgipbool,
- with_default (fn () => Bool.toString (! proofs >= 2)),
- (fn "false" => proofs := 1 | "true" => proofs := 2
- | x => error ("proof_option: illegal value: " ^ x)));
-
-val thm_deps_option = (pgipbool,
- with_default (fn () => Bool.toString (Output.has_mode thm_depsN)),
- (fn "false" => change print_mode (remove (op =) thm_depsN)
- | "true" => change print_mode (insert (op =) thm_depsN)
- | x => error ("thm_deps_option: illegal value: " ^ x)));
-
-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,
- with_default (fn () => string_of_int (! pg_print_depth_val)),
- (fn s => (case Syntax.read_nat s of
- NONE => error ("print_depth_option: illegal value: " ^ s)
- | 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",
- int_option ProofContext.prems_limit)),
- ("print-depth",
- ("Setting for the ML print depth",
- print_depth_option)),
- ("show-question-marks",
- ("Show leading question mark of variable name",
- bool_option show_question_marks))]),
- ("Tracing",
- [("trace-simplifier",
- ("Trace simplification rules.",
- bool_option trace_simp)),
- ("trace-simplifier-depth",
- ("Trace simplifier depth limit.",
- nat_option trace_simp_depth_limit)),
- ("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 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)),
- ("skip-proofs",
- ("Skip over proofs (interactive-only)",
- bool_option Toplevel.skip_proofs))])
- ];
-end;
-
-(** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
-
-fun lexicalstructure_keywords () =
- let val commands = OuterSyntax.dest_keywords ()
- fun category_of k = if (k mem commands) then "major" else "minor"
- (* NB: we might filter to only include words like elisp case (OuterSyntax.is_keyword). *)
- fun keyword_elt (keyword,help,kind,_) =
- XML.element "keyword" [("word", keyword), ("category", category_of kind)]
- [XML.element "shorthelp" [] [XML.text help]]
- in
- (* Also, note we don't call init_outer_syntax here to add interface commands,
- but they should never appear in scripts anyway so it shouldn't matter *)
- XML.element "lexicalstructure" [] (map keyword_elt (OuterSyntax.dest_parsers()))
- end
-
-(* TODO: we can issue a lexicalstructure/keyword when the syntax gets extended dynamically;
- hooks needed in outer_syntax.ML to do that. *)
-
-
-(* Configuration: GUI config, proverinfo messages *)
-
-
-fun orenv v d = case (getenv v) of "" => d | s => s
-
-local
- fun config_file() = orenv "ISABELLE_PGIPCONFIG" "~~/lib/ProofGeneral/pgip_isar.xml"
- fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" "http://isabelle.in.tum.de/"
-in
-fun send_pgip_config () =
- let
- val path = Path.explode (config_file())
- val exists = File.exists path
- val proverinfo =
- XML.element "proverinfo"
- [("name", "Isabelle"),
- ("version", version),
- ("instance", Session.name()),
- ("descr", "The Isabelle/Isar theorem prover"),
- ("url", isabelle_www()),
- ("filenameextns", ".thy;")]
- []
- in
- if exists then
- (issue_pgips [proverinfo];
- issue_pgips [File.read path];
- issue_pgips [lexicalstructure_keywords()])
- else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
- end;
-end
-
-
-(* Reveal some information about prover state *)
-fun send_informguise (openfile, opentheory, openproofpos) =
- let val guisefile =
- case openfile of SOME f => [XML.element "guisefile"
- [("url",Url.implode (Url.File (Path.explode f)))] []]
- | _ => []
- val guisetheory =
- case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
- | _ => []
- val guiseproof =
- case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
- | _ => []
- in
- issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
- 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
- fun pthm thy name = print_thm (get_thm thy (Name name))
-
- fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
-in
-(* FIXME: add askids for "file" here, which returns single theory with same name *)
-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 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)
-
-end
-
-
-
-(** Parsing proof scripts without execution **)
-
-(* Notes.
- This is quite tricky, because 1) we need to put back whitespace which
- was removed during parsing so we can provide markup around commands;
- 2) parsing is intertwined with execution in Isar so we have to repeat
- the parsing to extract interesting parts of commands. The trace of
- tokens parsed which is now recorded in each transition (added by
- Markus June '04) helps do this, but the mechanism is still a bad mess.
-
- If we had proper parse trees it would be easy, although having a
- fixed type of trees might be tricky with Isar's extensible parser.
-
- Probably the best solution is to produce the meta-information at
- the same time as the parse, for each command, e.g. by recording a
- list of (name,objtype) pairs which record the bindings created by
- a command. This would require changing the interfaces in
- outer_syntax.ML (or providing new ones),
-
- datatype metainfo = Binding of string * string (* name, objtype *)
-
- val command_withmetainfo: string -> string -> string ->
- (token list ->
- ((Toplevel.transition -> Toplevel.transition) * metainfo list) *
- token list) -> parser
-
- We'd also like to render terms as they appear in output, but this
- will be difficult because inner syntax is extensible and we don't
- have the correct syntax to hand when just doing outer parsing
- without execution. A reasonable approximation could
- perhaps be obtained by using the syntax of the current context.
- However, this would mean more mess trying to pick out terms,
- so at this stage a more serious change to the Isar functions
- seems necessary.
-*)
-
-local
- fun markup_text str elt = [XML.element elt [] [XML.text str]]
- fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
- fun empty elt = [XML.element elt [] []]
-
- fun whitespace str = XML.element "whitespace" [] [XML.text str]
-
- (* an extra token is needed to terminate the command *)
- val sync = OuterSyntax.scan "\\<^sync>";
-
- fun named_item_elt_with nameattr toks str elt nameP objtyp =
- let
- val name = (fst (nameP (toks@sync)))
- handle _ => (error ("Error occurred in name parser for " ^ elt ^
- "(objtype: " ^ objtyp ^ ")");
- "")
-
- in
- [XML.element elt
- ((if name="" then [] else [(nameattr, name)])@
- (if objtyp="" then [] else [("objtype", objtyp)]))
- ([XML.text str])]
- end
-
- val named_item_elt = named_item_elt_with "name"
- val thmnamed_item_elt = named_item_elt_with "thmname"
-
- fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
-
- (* FIXME: allow dynamic extensions to language here: we need a hook in
- outer_syntax.ML to reset this table. *)
-
- val keywords_classification_table = ref (NONE: string Symtab.table option)
-
- fun get_keywords_classification_table () =
- case (!keywords_classification_table) of
- SOME t => t
- | NONE => (let
- val tab = fold (fn (c, _, k, _) => Symtab.update (c, k))
- (OuterSyntax.dest_parsers ()) Symtab.empty;
- in (keywords_classification_table := SOME tab; tab) end)
-
-
-
- fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
- let
- val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
- in
- markup_text_attrs str "opentheory"
- ([("thyname",thyname)] @
- (if imports=[] then [] else
- [("parentnames", (space_implode ";" imports) ^ ";")]))
- end
-
- fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases *)
- let
- (* NB: PGIP only deals with single name bindings at the moment;
- potentially we could markup grouped definitions several times but
- that might suggest the wrong structure to the editor?
- Better alternative would be to put naming closer around text,
- but to do that we'd be much better off modifying the real parser
- instead of reconstructing it here. *)
-
- val plain_items = (* no names, unimportant names, or too difficult *)
- ["defaultsort","arities","judgement","finalconsts",
- "syntax", "nonterminals", "translations",
- "global", "local", "hide",
- "ML_setup", "setup", "method_setup",
- "parse_ast_translation", "parse_translation", "print_translation",
- "typed_print_translation", "print_ast_translation", "token_translation",
- "oracle",
- "declare"]
-
- val plain_item = markup_text str "theoryitem"
- val comment_item = markup_text str "doccomment"
- val named_item = named_item_elt toks str "theoryitem"
-
- val opt_overloaded = P.opt_keyword "overloaded";
-
- val thmnameP = (* see isar_syn.ML/theoremsP *)
- let
- val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
- val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
- in
- theoremsP
- end
- in
- (* TODO: ideally we would like to render terms properly, just as they are
- in output. This implies using PGML for symbols and variables/atoms.
- BUT it's rather tricky without having the correct concrete syntax to hand,
- and even if we did, we'd have to mess around here a whole lot more first
- to pick out the terms from the syntax. *)
-
- if member (op =) plain_items name then plain_item
- else case name of
- "text" => comment_item
- | "text_raw" => comment_item
- | "typedecl" => named_item (P.type_args |-- P.name) "type"
- | "types" => named_item (P.type_args |-- P.name) "type"
- | "classes" => named_item P.name "class"
- | "classrel" => named_item P.name "class"
- | "consts" => named_item (P.const >> #1) "term"
- | "axioms" => named_item (P.spec_name >> (#1 o #1)) "theorem"
- | "defs" => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
- | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
- | "theorems" => named_item thmnameP "thmset"
- | "lemmas" => named_item thmnameP "thmset"
- | "oracle" => named_item P.name "oracle"
- | "locale" => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
- | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
- end
-
- fun xmls_of_thy_goal (name,toks,str) =
- let
- (* see isar_syn.ML/gen_theorem *)
- val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
- val general_statement =
- statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
-
- val gen_theoremP =
- P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
- Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
- general_statement >> (fn ((locale, a), (elems, concl)) =>
- fst a) (* a : (bstring * Args.src list) *)
-
- val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
- (* TODO: add preference values for attributes
- val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
- *)
- in
- (thmnamed_item_elt toks str "opengoal" nameP "") @
- (empty "openblock")
- end
-
- fun xmls_of_qed (name,markup) =
- let val qedmarkup =
- (case name of
- "sorry" => markup "postponegoal"
- | "oops" => markup "giveupgoal"
- | "done" => markup "closegoal"
- | "by" => markup "closegoal" (* nested or toplevel *)
- | "qed" => markup "closegoal" (* nested or toplevel *)
- | "." => markup "closegoal" (* nested or toplevel *)
- | ".." => markup "closegoal" (* nested or toplevel *)
- | other => (* default to closegoal: may be wrong for extns *)
- (parse_warning
- ("Unrecognized qed command: " ^ quote other);
- markup "closegoal"))
- in qedmarkup @ (empty "closeblock") end
-
- fun xmls_of_kind kind (name,toks,str) =
- let val markup = markup_text str in
- case kind of
- "control" => markup "badcmd"
- | "diag" => markup "spuriouscmd"
- (* theory/files *)
- | "theory-begin" => xmls_of_thy_begin (name,toks,str)
- | "theory-decl" => xmls_of_thy_decl (name,toks,str)
- | "theory-heading" => markup "doccomment"
- | "theory-script" => markup "theorystep"
- | "theory-end" => markup "closetheory"
- (* proof control *)
- | "theory-goal" => xmls_of_thy_goal (name,toks,str)
- | "proof-heading" => markup "doccomment"
- | "proof-goal" => (markup "opengoal") @ (empty "openblock") (* nested proof: have, show, ... *)
- | "proof-block" => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
- | "proof-open" => (empty "openblock") @ (markup "proofstep")
- | "proof-close" => (markup "proofstep") @ (empty "closeblock")
- | "proof-script" => markup "proofstep"
- | "proof-chain" => markup "proofstep"
- | "proof-decl" => markup "proofstep"
- | "proof-asm" => markup "proofstep"
- | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock") (* nested proof: obtain *)
- | "qed" => xmls_of_qed (name,markup)
- | "qed-block" => xmls_of_qed (name,markup)
- | "qed-global" => xmls_of_qed (name,markup)
- | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
- (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
- markup "spuriouscmd")
- end
-in
-
-fun xmls_of_transition (name,str,toks) =
- let
- val classification = Symtab.lookup (get_keywords_classification_table ()) name
- in case classification of
- SOME k => (xmls_of_kind k (name,toks,str))
- | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
- (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
- markup_text str "spuriouscmd")
- end
-
-fun markup_toks [] _ = []
- | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x
-
-fun markup_comment_whs [] = []
- | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
- let
- val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
- in
- if (prewhs <> []) then
- whitespace (implode (map OuterLex.unparse prewhs))
- :: (markup_comment_whs rest)
- else
- (markup_text (OuterLex.unparse t) "comment") @
- (markup_comment_whs ts)
- end
-
-fun xmls_pre_cmd [] = ([],[])
- | xmls_pre_cmd toks =
- let
- (* an extra token is needed to terminate the command *)
- val sync = OuterSyntax.scan "\\<^sync>";
- val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
- val text_with_whs =
- ((spaceP || Scan.succeed "") --
- (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
- -- (spaceP || Scan.succeed "") >> op^
- val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
- (* NB: this collapses litcomment,(litcomment|whitespace)* to a single litcomment *)
- val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
- val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
- in
- ((markup_comment_whs prewhs) @
- (if (length rest2 = length rest1) then []
- else markup_text (implode
- (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
- "doccomment") @
- (markup_comment_whs postwhs),
- Library.take (length rest3 - 1,rest3))
- end
-
-fun xmls_of_impropers toks =
- let
- val (xmls,rest) = xmls_pre_cmd toks
- in
- xmls @ (markup_toks rest "unparseable")
- end
-
-fun markup_unparseable str = markup_text str "unparseable"
-
-end
-
-
-local
- (* we have to weave together the whitespace/comments with proper tokens
- to reconstruct the input. *)
- (* TODO: see if duplicating isar_output/parse_thy can help here *)
-
- fun match_tokens ([],us,vs) = (rev vs,us) (* used, unused *)
- | match_tokens (t::ts,w::ws,vs) =
- if (t = w) then match_tokens (ts,ws,w::vs)
- else match_tokens (t::ts,ws,w::vs)
- | match_tokens _ = error ("match_tokens: mismatched input parse")
-in
- fun xmls_of_str str =
- let
- (* parsing: See outer_syntax.ML/toplevel_source *)
- fun parse_loop ([],[],xmls) = xmls
- | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
- | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
- let
- (* first proper token after whitespace/litcomment/whitespace is command *)
- val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
- val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
- | _ => error("proof_general/parse_loop impossible")
- val (utoks,itoks'') = match_tokens (toks,itoks',[])
- (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
-
- val str = implode (map OuterLex.unparse (cmdtok::utoks))
-
- val xmls_tr = xmls_of_transition (nm,str,toks)
- in
- parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
- end
- in
- (let val toks = OuterSyntax.scan str
- in
- parse_loop (OuterSyntax.read toks, toks, [])
- end)
- handle _ => markup_unparseable str
- end
-
-
-fun parsescript str attrs =
- let
- val _ = start_delay_msgs () (* accumulate error messages to put inside parseresult *)
- val xmls = xmls_of_str str
- val errs = end_delayed_msgs ()
- in
- issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
- end
-end
-
-
-
-(**** PGIP: Isabelle -> Interface ****)
-
-val isabelle_pgml_version_supported = "1.0";
-val isabelle_pgip_version_supported = "2.0"
-
-(* TODO: would be cleaner to define a datatype here for the accepted elements,
- and mapping functions to/from strings. At the moment this list must
- coincide with the strings in the function process_pgip_element. *)
-val isabelle_acceptedpgipelems =
- ["askpgip","askpgml","askprefs","getpref","setpref",
- "proverinit","proverexit","startquiet","stopquiet",
- "pgmlsymbolson", "pgmlsymbolsoff",
- "dostep", "undostep", "redostep", "abortgoal", "forget", "restoregoal",
- "askids", "showid", "askguise",
- "parsescript",
- "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
- "doitem", "undoitem", "redoitem", "abortheory",
- "retracttheory", "loadfile", "openfile", "closefile",
- "abortfile", "retractfile", "changecwd", "systemcmd"];
-
-fun usespgip () =
- issue_pgip
- "usespgip"
- [("version", isabelle_pgip_version_supported)]
- (XML.element "acceptedpgipelems" []
- (map (fn s=>XML.element "pgipelem"
- [] (* if threads: possibility to add async here *)
- [s])
- isabelle_acceptedpgipelems))
-
-fun usespgml () =
- issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)]
-
-fun hasprefs () =
- List.app (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 () = maps snd (!preferences)
-
-fun setpref name value =
- (case AList.lookup (op =) (allprefs ()) name of
- NONE => warning ("Unknown pref: " ^ quote name)
- | SOME (_, (_, _, set)) => set value);
-
-fun getpref name =
- (case AList.lookup (op =) (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 *)
-
-fun isarcmd s =
- s |> OuterSyntax.scan |> OuterSyntax.read
- |> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;
-
-fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
- | xmltext [] = ""
- | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
-
-fun isarscript xmls = isarcmd (xmltext xmls) (* send a script command *)
-
-
-(* load an arbitrary file (must be .thy or .ML) *)
-
-fun use_thy_or_ml_file file =
- let
- val (path,extn) = Path.split_ext (Path.explode file)
- in
- case extn of
- "" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
- | "thy" => isarcmd ("use_thy " ^ (quote (Path.implode path)))
- | "ML" => isarcmd ("use " ^ quote file)
- | other => error ("Don't know how to read a file with extension " ^ other)
- end
-
-
-(* Proof control commands *)
-
-local
- fun xmlattro attr attrs = AList.lookup (op =) attrs attr
-
- fun xmlattr attr attrs =
- (case xmlattro attr attrs of
- SOME value => value
- | NONE => raise PGIP ("Missing attribute: " ^ attr))
-
- val thyname_attro = xmlattro "thyname"
- val thyname_attr = xmlattr "thyname"
- val objtype_attro = xmlattro "objtype"
- val objtype_attr = xmlattr "objtype"
- val name_attr = xmlattr "name"
-
- fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
- case Url.explode url of
- (Url.File path) => File.platform_path path
- | _ => error ("Cannot access non-local URL " ^ url)
-
- val fileurl_of = localfile_of_url o (xmlattr "url")
-
- val topthy = Toplevel.theory_of o Toplevel.get_state
- val topthy_name = Context.theory_name o topthy
-
- val currently_open_file = ref (NONE : string option)
-
- (* Path management: we allow theory files to have dependencies
- in their own directory, but when we change directory for a new
- file we remove the path. Leaving it there can cause confusion
- with difference in batch mode. NB: PGIP does not currently assume
- that the prover has a load path. *)
- local
- val current_working_dir = ref (NONE : string option)
- in
- fun changecwd dir =
- (case (!current_working_dir) of
- NONE => ()
- | SOME dir => ThyLoad.del_path dir;
- ThyLoad.add_path dir;
- current_working_dir := SOME dir)
- end
-
- fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
-in
-
-fun process_pgip_element pgipxml = (case pgipxml of
- (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
-| (xml as (XML.Elem (elem, attrs, data))) =>
- (case elem of
- (* protocol config *)
- "askpgip" => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
- usespgip (); send_pgip_config ())
- | "askpgml" => usespgml ()
- (* proverconfig *)
- | "askprefs" => hasprefs ()
- | "getpref" => getpref (name_attr attrs)
- | "setpref" => setpref (name_attr attrs) (xmltext data)
- (* provercontrol *)
- | "proverinit" => isar_restart ()
- | "proverexit" => isarcmd "quit"
- | "startquiet" => isarcmd "disable_pr"
- | "stopquiet" => isarcmd "enable_pr"
- | "pgmlsymbolson" => change print_mode (fn mode =>
- remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
- | "pgmlsymbolsoff" => change print_mode (remove (op =) Symbol.xsymbolsN)
- (* properproofcmd: proper commands which belong in script *)
- (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
- (* NB: Isar doesn't make lemma name of goal accessible during proof *)
- | "opengoal" => isarscript data
- | "proofstep" => isarscript data
- | "closegoal" => isarscript data
- | "giveupgoal" => isarscript data
- | "postponegoal" => isarscript data
- | "comment" => isarscript data
- | "doccomment" => isarscript data
- | "whitespace" => isarscript data (* NB: should be ignored, but process anyway *)
- | "litcomment" => isarscript data (* NB: should be ignored, process for back compat *)
- | "spuriouscmd" => isarscript data
- | "badcmd" => isarscript data
- (* improperproofcmd: improper commands which *do not* belong in script *)
- | "dostep" => isarscript data
- | "undostep" => isarcmd "undos_proof 1"
- | "redostep" => isarcmd "redo"
- | "abortgoal" => isarcmd "ProofGeneral.kill_proof"
- | "forget" => error "Not implemented"
- | "restoregoal" => error "Not implemented" (* could just treat as forget? *)
- (* proofctxt: improper commands *)
- | "askids" => askids (thyname_attro attrs, objtype_attro attrs)
- | "showid" => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
- | "askguise" => send_informguise (!currently_open_file,
- SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
- topproofpos())
- | "parsescript" => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
- | "showproofstate" => isarcmd "pr"
- | "showctxt" => isarcmd "print_theory" (* more useful than print_context *)
- | "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data)
- | "setlinewidth" => isarcmd ("pretty_setmargin " ^ xmltext data)
- | "viewdoc" => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *)
- (* properfilecmd: proper theory-level script commands *)
- (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
- | "opentheory" => isarscript data
- | "theoryitem" => isarscript data
- | "closetheory" => let
- val thyname = topthy_name()
- in (isarscript data;
- writeln ("Theory " ^ quote thyname ^ " completed."))
- end
- (* improperfilecmd: theory-level commands not in script *)
- | "doitem" => isarscript data
- | "undoitem" => isarcmd "ProofGeneral.undo" (* NB: named target not supported *)
- | "redoitem" => isarcmd "ProofGeneral.redo"
- | "aborttheory" => isarcmd ("init_toplevel")
- | "retracttheory" => isarcmd ("kill_thy " ^ quote (thyname_attr attrs))
- | "loadfile" => (case !currently_open_file of
- SOME f => raise PGIP ("loadfile when a file is open!")
- | NONE => use_thy_or_ml_file (fileurl_of attrs))
- | "openfile" => (case !currently_open_file of
- SOME f => raise PGIP ("openfile when a file is already open!")
- | NONE => (openfile_retract (fileurl_of attrs);
- currently_open_file := SOME (fileurl_of attrs)))
- | "closefile" => (case !currently_open_file of
- SOME f => (proper_inform_file_processed f (Isar.state());
- currently_open_file := NONE)
- | NONE => raise PGIP ("closefile when no file is open!"))
- | "abortfile" => (case !currently_open_file of
- SOME f => (isarcmd "init_toplevel";
- currently_open_file := NONE)
- | NONE => raise PGIP ("abortfile when no file is open!"))
- | "retractfile" => (case !currently_open_file of
- SOME f => raise PGIP ("retractfile when a file is open!")
- | NONE => inform_file_retracted (fileurl_of attrs))
- | "changecwd" => changecwd (fileurl_of attrs)
- | "systemcmd" => isarscript data
- (* unofficial command for debugging *)
- | "quitpgip" => raise PGIP_QUIT
- | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
-
-fun process_pgip_tree xml =
- (pgip_refid := NONE;
- pgip_refseq := NONE;
- (case xml of
- XML.Elem ("pgip", attrs, pgips) =>
- (let
- val class = xmlattr "class" attrs
- val dest = xmlattro "destid" attrs
- val _ = (pgip_refid := xmlattro "id" attrs;
- pgip_refseq := xmlattro "seq" attrs)
- in
- (* We respond to broadcast messages to provers, or
- messages intended uniquely for us. Silently ignore rest. *)
- case dest of
- NONE => if (class = "pa") then
- (List.app process_pgip_element pgips; true)
- else false
- | SOME id => if (matching_pgip_id id) then
- (List.app process_pgip_element pgips; true)
- else false
- end)
- | _ => raise PGIP "Invalid PGIP packet received")
- handle PGIP msg =>
- error (msg ^ "\nPGIP error occured in XML text below:\n" ^
- (XML.string_of_tree xml)))
-
-val process_pgip = K () o process_pgip_tree o XML.tree_of_string
-
-end
-
-
-(* PGIP loop: process PGIP input only *)
-
-local
-
-exception XML_PARSE
-
-fun loop ready src =
- let
- val _ = if ready then (issue_pgipe "ready" []) else ()
- val pgipo = (Source.get_single src)
- handle e => raise XML_PARSE
- in
- case pgipo of
- NONE => ()
- | SOME (pgip,src') =>
- let
- val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true)
- in
- loop ready' src'
- end
- end handle e => handler (e,SOME src) (* i.e. error in ready/XML parse *)
-
-and handler (e,srco) =
- case (e,srco) of
- (XML_PARSE,SOME src) =>
- Output.panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
- | (PGIP_QUIT,_) => ()
- | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src)
- | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *)
- | (e,SOME src) => (error (Toplevel.exn_message e); loop true src)
- | (_,NONE) => ()
-in
- (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
-
- val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
-
- val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
-
- fun pgip_toplevel x = loop true x
-end
-
-
-(* additional outer syntax for Isar *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val undoP = (*undo without output*)
- OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
- (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
-
-val redoP = (*redo without output*)
- OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
- (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
-
-val context_thy_onlyP =
- OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
- (P.name >> (Toplevel.no_timing oo IsarCmd.init_context update_thy_only));
-
-val try_context_thy_onlyP =
- OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
- (P.name >> (Toplevel.no_timing oo
- (Toplevel.imperative (K ()) oo IsarCmd.init_context try_update_thy_only)));
-
-val restartP =
- OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
- (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
-
-val kill_proofP =
- OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
- (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
-
-val inform_file_processedP =
- OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
- (P.name >> (fn file => Toplevel.no_timing o
- Toplevel.keep (vacuous_inform_file_processed file) o
- Toplevel.kill o
- Toplevel.keep (proper_inform_file_processed file)));
-
-val inform_file_retractedP =
- OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
- (P.name >> (Toplevel.no_timing oo
- (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
-
-val process_pgipP =
- OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
- (P.text >> (Toplevel.no_timing oo
- (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
-
-fun init_outer_syntax () = OuterSyntax.add_parsers
- [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
- inform_file_processedP, inform_file_retractedP, process_pgipP];
-
-end;
-
-
-(* init *)
-
-val initialized = ref false;
-
-fun set_prompts true _ = ml_prompts "ML> " "ML# "
- | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
- | set_prompts false false = ml_prompts ("> " ^ special "372") ("- " ^ special "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 ();
- setup_present_hook ();
- set initialized; ()));
- sync_thy_loader ();
- change print_mode (cons proof_generalN o remove (op =) proof_generalN);
- init_pgip_session_id ();
- if pgip then
- change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN])
- else
- pgip_emacs_compatibility_flag := true; (* assume this for PG <3.6 compatibility *)
- set_prompts isar pgip;
- pgip_active := pgip);
-
-fun init isar =
- (init_setup isar false;
- if isar then Isar.sync_main () else isa_restart ());
-
-fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
- | init_pgip true = (init_setup true true; pgip_toplevel tty_src);
-
-
-
-(** generate elisp file for keyword classification **)
-
-local
-
-val regexp_meta = member (op =) (explode ".*+?[]^$");
-val regexp_quote =
- implode o map (fn c => if regexp_meta c 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
- (commands |> map_filter (fn (c, _, k, _) => if k = kind then SOME c else NONE));
-
-fun make_elisp_syntax (keywords, commands) =
- ";;\n\
- \;; Keyword classification tables for Isabelle/Isar.\n\
- \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
- \;;\n\
- \;; $" ^ "Id$\n\
- \;;\n" ^
- defconst "major" (map #1 commands) ^
- defconst "minor" (List.filter Syntax.is_identifier keywords) ^
- implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^
- "\n(provide 'isar-keywords)\n";
-
-in
-
-fun write_keywords s =
- (init_outer_syntax ();
- File.write (Path.explode ("isar-keywords" ^ (if s = "" then "" else "-" ^ s) ^".el"))
- (make_elisp_syntax (OuterSyntax.dest_keywords (), OuterSyntax.dest_parsers ())));
-
-end;
-
-
-end;
-
-structure ProofGeneralPgip = ProofGeneral; (* for forward compatibility *)