# HG changeset patch # User wenzelm # Date 1167413146 -3600 # Node ID fbd068dd4d29618221cbdf87a01c9633d8062228 # Parent 9b772ac66830ae1eb6746e4579213e9d8661c7dd minor tuning; diff -r 9b772ac66830 -r fbd068dd4d29 src/Pure/ProofGeneral/pgip_input.ML --- a/src/Pure/ProofGeneral/pgip_input.ML Fri Dec 29 18:25:45 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_input.ML Fri Dec 29 18:25:46 2006 +0100 @@ -2,7 +2,7 @@ ID: $Id$ Author: David Aspinall -PGIP abstraction: input commands +PGIP abstraction: input commands. *) signature PGIPINPUT = @@ -146,7 +146,7 @@ val times_attr = read_pgipnat o (get_attr_dflt "times" "1") val prefcat_attr = get_attr_opt "prefcategory" - fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts) + fun xmltext (XML.Text text :: ts) = text ^ xmltext ts | xmltext [] = "" | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)" diff -r 9b772ac66830 -r fbd068dd4d29 src/Pure/ProofGeneral/pgip_isabelle.ML --- a/src/Pure/ProofGeneral/pgip_isabelle.ML Fri Dec 29 18:25:45 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Fri Dec 29 18:25:46 2006 +0100 @@ -2,7 +2,7 @@ ID: $Id$ Author: David Aspinall -Prover-side PGIP abstraction: Isabelle configuration +Prover-side PGIP abstraction: Isabelle configuration. *) signature PGIP_ISABELLE = diff -r 9b772ac66830 -r fbd068dd4d29 src/Pure/ProofGeneral/pgip_output.ML --- a/src/Pure/ProofGeneral/pgip_output.ML Fri Dec 29 18:25:45 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_output.ML Fri Dec 29 18:25:46 2006 +0100 @@ -2,7 +2,7 @@ ID: $Id$ Author: David Aspinall -PGIP abstraction: output commands +PGIP abstraction: output commands. *) signature PGIPOUTPUT = @@ -110,7 +110,7 @@ let val area = #area vs in - XML.Elem ("cleardisplay", (attrs_of_displayarea area), []) + XML.Elem ("cleardisplay", attrs_of_displayarea area, []) end fun normalresponse (Normalresponse vs) = @@ -121,9 +121,9 @@ val content = #content vs in XML.Elem ("normalresponse", - (attrs_of_displayarea area) @ + attrs_of_displayarea area @ (if urgent then attr "urgent" "true" else []) @ - (attrs_of_messagecategory messagecategory), + attrs_of_messagecategory messagecategory, content) end @@ -135,9 +135,9 @@ val content = #content vs in XML.Elem ("errorresponse", - (the_default [] (Option.map attrs_of_displayarea area)) @ - (attrs_of_fatality fatality) @ - (the_default [] (Option.map attrs_of_location location)), + these (Option.map attrs_of_displayarea area) @ + attrs_of_fatality fatality @ + these (Option.map attrs_of_location location), content) end @@ -267,7 +267,7 @@ val errs = #errs vs val xmldoc = PgipMarkup.output_doc doc in - XML.Elem("parseresult", attrs, errs@xmldoc) + XML.Elem("parseresult", attrs, errs @ xmldoc) end fun acceptedpgipelems (Usespgip vs) = diff -r 9b772ac66830 -r fbd068dd4d29 src/Pure/ProofGeneral/pgip_tests.ML --- a/src/Pure/ProofGeneral/pgip_tests.ML Fri Dec 29 18:25:45 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_tests.ML Fri Dec 29 18:25:46 2006 +0100 @@ -3,7 +3,7 @@ Author: David Aspinall A test suite for the PGIP abstraction code (in progress). -Run to provide some mild insurance against breakage in Isabelle/here. +Run to provide some mild insurance against breakage in Isabelle here. *) (** pgip_types.ML **) @@ -70,7 +70,7 @@ open PgipInput; fun asseqi a b = - if (input (e a))=b then () + if input (e a) = b then () else error("PGIP test: expected two inputs to be equal, for input:\n" ^ a) in @@ -103,7 +103,7 @@ open PgipMarkup open PgipParser fun asseqp a b = - if (pgip_parser a)=b then () + if pgip_parser a = b then () else error("PGIP test: expected two parses to be equal, for input:\n" ^ a) in diff -r 9b772ac66830 -r fbd068dd4d29 src/Pure/ProofGeneral/pgip_types.ML --- a/src/Pure/ProofGeneral/pgip_types.ML Fri Dec 29 18:25:45 2006 +0100 +++ b/src/Pure/ProofGeneral/pgip_types.ML Fri Dec 29 18:25:46 2006 +0100 @@ -2,7 +2,7 @@ ID: $Id$ Author: David Aspinall -PGIP abstraction: types and conversions +PGIP abstraction: types and conversions. *) (* TODO: PGML *) @@ -152,7 +152,7 @@ | ObjType => "type" | ObjOther s => s -val attrs_of_objtype = (attr "objtype") o name_of_objtype +val attrs_of_objtype = attr "objtype" o name_of_objtype fun objtype_of_attrs attrs = case get_attr "objtype" attrs of "file" => ObjFile @@ -289,7 +289,7 @@ XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs)) end -val pgiptype_to_xml = pgipdtype_to_xml o (pair NONE) +val pgiptype_to_xml = pgipdtype_to_xml o pair NONE fun read_pguval Pgipnull s = if s="" then Pgvalnull @@ -306,7 +306,7 @@ | read_pguval (Pgipchoice tydescs) s = let (* Union type: match first in list *) - fun getty (Pgipdtype(_,ty)) = ty + fun getty (Pgipdtype(_, ty)) = ty val uval = get_first (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE) (map getty tydescs) @@ -318,11 +318,11 @@ fun read_pgval ty s = (ty, read_pguval ty s) fun pgval_to_string (_, Pgvalnull) = "" - | pgval_to_string (_,(Pgvalbool b)) = bool_to_pgstring b - | pgval_to_string (_,(Pgvalnat n)) = int_to_pgstring n - | pgval_to_string (_,(Pgvalint i)) = int_to_pgstring i - | pgval_to_string (_,(Pgvalconst c)) = string_to_pgstring c - | pgval_to_string (_,(Pgvalstring s)) = string_to_pgstring s + | pgval_to_string (_, Pgvalbool b) = bool_to_pgstring b + | pgval_to_string (_, Pgvalnat n) = int_to_pgstring n + | pgval_to_string (_, Pgvalint i) = int_to_pgstring i + | pgval_to_string (_, Pgvalconst c) = string_to_pgstring c + | pgval_to_string (_, Pgvalstring s) = string_to_pgstring s type pgipurl = Path.T (* URLs: only local files *) @@ -356,7 +356,7 @@ fun attrs_of_pgipurl purl = [("url", "file:" ^ (XML.text (File.platform_path (File.full_path purl))))] -val pgipurl_of_attrs = pgipurl_of_string o (get_attr "url") +val pgipurl_of_attrs = pgipurl_of_string o get_attr "url" fun pgipurl_of_url (Url.File p) = p | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.implode url)) @@ -392,8 +392,8 @@ fun attrs_of_location ({ descr, url, line, column, char }:location) = let - val descr = opt_attr "descr"descr - val url = the_default [] (Option.map attrs_of_pgipurl url) + val descr = opt_attr "descr" descr + val url = these (Option.map attrs_of_pgipurl url) val line = opt_attr_map int_to_pgstring "line" line val column = opt_attr_map int_to_pgstring "column" column val char = opt_attr_map int_to_pgstring "char" char diff -r 9b772ac66830 -r fbd068dd4d29 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Fri Dec 29 18:25:45 2006 +0100 +++ b/src/Pure/ProofGeneral/preferences.ML Fri Dec 29 18:25:46 2006 +0100 @@ -52,7 +52,7 @@ val proof_pref = let fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2) - fun set s = proofs := (if (PgipTypes.read_pgipbool s) then 1 else 2) + fun set s = proofs := (if PgipTypes.read_pgipbool s then 1 else 2) in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" @@ -61,7 +61,7 @@ val thm_deps_pref = let fun get () = PgipTypes.bool_to_pgstring (Output.has_mode thm_depsN) - fun set s = if (PgipTypes.read_pgipbool s) then + fun set s = if PgipTypes.read_pgipbool s then change print_mode (insert (op =) thm_depsN) else change print_mode (remove (op =) thm_depsN) @@ -143,7 +143,7 @@ "Take a few short cuts", bool_pref Toplevel.skip_proofs "skip-proofs" - "Ignore proof scripts (interactive-only)"] + "Skip over proofs (interactive-only)"] val preferences = [("Display", display_preferences), diff -r 9b772ac66830 -r fbd068dd4d29 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Dec 29 18:25:45 2006 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Dec 29 18:25:46 2006 +0100 @@ -9,7 +9,7 @@ signature PROOF_GENERAL = sig val init: bool -> unit - val init_pgip: bool -> unit (* for compatibility; always fails *) + val init_pgip: bool -> unit (* for compatibility; always fails *) val write_keywords: string -> unit end; @@ -22,7 +22,6 @@ val proof_generalN = "ProofGeneralEmacs"; (*token markup (colouring vars, etc.)*) val pgasciiN = "PGASCII"; (*plain 7-bit ASCII communication*) -val xsymbolsN = Symbol.xsymbolsN; (*X-Symbol symbols*) val thm_depsN = "thm_deps"; (*meta-information about theorem deps*) fun special oct = @@ -38,7 +37,7 @@ | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s; fun xsymbols_output s = - if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then + 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; @@ -46,7 +45,7 @@ in fun setup_xsymbols_output () = - Output.add_mode xsymbolsN + Output.add_mode Symbol.xsymbolsN (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw); end; @@ -119,18 +118,16 @@ fun emacs_notify s = decorate (special "360") (special "361") "" s; fun tell_clear_goals () = - emacs_notify "Proof General, please clear the goals buffer."; + emacs_notify "Proof General, please clear the goals buffer."; fun tell_clear_response () = - emacs_notify "Proof General, please clear the response buffer."; + emacs_notify "Proof General, please clear the response buffer."; fun tell_file_loaded path = - emacs_notify ("Proof General, this file is loaded: " ^ - quote (File.platform_path path)); + emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path)); fun tell_file_retracted path = - emacs_notify ("Proof General, you can unlock the file " - ^ quote (File.platform_path path)); + emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path)); (* theory / proof state output *) @@ -221,11 +218,11 @@ val welcome = priority o Session.welcome; fun restart () = - (sync_thy_loader (); - tell_clear_goals (); - tell_clear_response (); - welcome (); - raise Toplevel.RESTART) + (sync_thy_loader (); + tell_clear_goals (); + tell_clear_response (); + welcome (); + raise Toplevel.RESTART); (* theorem dependency output *) @@ -316,27 +313,25 @@ fun set_prompts () = ml_prompts "ML> " "ML# " -fun init_setup () = - (conditional (not (! initialized)) (fn () => - (setmp warning_fn (K ()) init_outer_syntax (); - setup_xsymbols_output (); - setup_messages (); - ProofGeneralPgip.init_pgip_channel (!priority_fn); - setup_state (); - setup_thy_loader (); - setup_present_hook (); - set initialized; ())); - sync_thy_loader (); - change print_mode (cons proof_generalN o remove (op =) proof_generalN); - set_prompts ()) - -fun init true = (init_setup (); - Isar.sync_main ()) - | init false = Output.panic "Interface support no longer available for Isabelle/classic mode." +fun init false = + Output.panic "Interface support no longer available for Isabelle/classic mode." + | init true = + (conditional (not (! initialized)) (fn () => + (setmp warning_fn (K ()) init_outer_syntax (); + setup_xsymbols_output (); + setup_messages (); + ProofGeneralPgip.init_pgip_channel (! priority_fn); + setup_state (); + setup_thy_loader (); + setup_present_hook (); + set initialized; ())); + sync_thy_loader (); + change print_mode (cons proof_generalN o remove (op =) proof_generalN); + set_prompts (); + Isar.sync_main ()); fun init_pgip false = init true - | init_pgip true = Output.panic "No PGIP here, please use ProofGeneralPgip.init_pgip (update your isabelle-process script)." - + | init_pgip true = Output.panic "No PGIP here, please use ProofGeneralPgip.init_pgip." @@ -345,8 +340,7 @@ 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; +val regexp_quote = translate_string (fn c => if regexp_meta c then "\\\\" ^ c else c); fun defconst name strs = "\n(defconst isar-keywords-" ^ name ^ @@ -363,7 +357,7 @@ \;; $" ^ "Id$\n\ \;;\n" ^ defconst "major" (map #1 commands) ^ - defconst "minor" (List.filter Syntax.is_identifier keywords) ^ + defconst "minor" (filter Syntax.is_identifier keywords) ^ implode (map (make_elisp_commands commands) OuterKeyword.kinds) ^ "\n(provide 'isar-keywords)\n"; @@ -376,5 +370,4 @@ end; - end; diff -r 9b772ac66830 -r fbd068dd4d29 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Dec 29 18:25:45 2006 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Dec 29 18:25:46 2006 +0100 @@ -3,17 +3,17 @@ Author: David Aspinall and Markus Wenzel Isabelle configuration for Proof General using PGIP protocol. -See http://proofgeneral.inf.ed.ac.uk/kit +See http://proofgeneral.inf.ed.ac.uk/kit *) signature PROOF_GENERAL_PGIP = sig - val init_pgip: bool -> unit (* main PGIP loop with true; fail with false *) + val init_pgip: bool -> unit (* main PGIP loop with true; fail with false *) (* These two are just to support the semi-PGIP Emacs mode *) - val init_pgip_channel: (string -> unit) -> unit - val process_pgip: string -> unit + val init_pgip_channel: (string -> unit) -> unit + val process_pgip: string -> unit end structure ProofGeneralPgip : PROOF_GENERAL_PGIP = @@ -26,7 +26,6 @@ (* print modes *) val proof_generalN = "ProofGeneral"; (*token markup (colouring vars, etc.)*) -val xsymbolsN = Symbol.xsymbolsN; (*X-Symbol 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*) @@ -40,7 +39,7 @@ | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s; fun xsymbols_output s = - if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then + 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; @@ -49,7 +48,7 @@ fun pgml_sym s = (case Symbol.decode s of Symbol.Char s => XML.text s - | Symbol.Sym sn => XML.element "sym" [("name", sn)] [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); @@ -60,7 +59,7 @@ in fun setup_xsymbols_output () = - Output.add_mode xsymbolsN + Output.add_mode Symbol.xsymbolsN (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw); fun setup_pgml_output () = @@ -84,7 +83,7 @@ fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x]; -fun tagit kind x = +fun tagit kind x = (xml_atom kind x, real (Symbol.length (Symbol.explode x))); fun free_or_skolem x = @@ -130,15 +129,15 @@ fun pgip_serial () = inc pgip_seq fun assemble_pgips pgips = - Pgip { tag = SOME pgip_tag, - class = pgip_class, - seq = pgip_serial(), - id = !pgip_id, - destid = !pgip_refid, - (* destid=refid since Isabelle only communicates back to sender *) - refid = !pgip_refid, - refseq = !pgip_refseq, - content = pgips } + Pgip { tag = SOME pgip_tag, + class = pgip_class, + seq = pgip_serial(), + id = !pgip_id, + destid = !pgip_refid, + (* destid=refid since Isabelle only communicates back to sender *) + refid = !pgip_refid, + refseq = !pgip_refseq, + content = pgips } in fun init_pgip_session_id () = @@ -147,10 +146,10 @@ fun matching_pgip_id id = (id = !pgip_id) -val output_xml_fn = ref writeln_default +val output_xml_fn = ref writeln_default fun output_xml s = (!output_xml_fn) (XML.string_of_tree s); (* TODO: string buffer *) -fun issue_pgip_rawtext str = +fun issue_pgip_rawtext str = output_xml (PgipOutput.output (assemble_pgips [XML.Rawtext str])) fun issue_pgips pgipops = @@ -169,29 +168,29 @@ val delayed_msgs = ref [] fun queue_or_issue pgip = - if (! delay_msgs) then - delayed_msgs := pgip :: ! delayed_msgs - else issue_pgip pgip + if ! delay_msgs then + delayed_msgs := pgip :: ! delayed_msgs + else issue_pgip pgip in - fun normalmsg area cat urgent s = - let - val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) - val pgip = Normalresponse {area=area,messagecategory=cat, - urgent=urgent,content=[content] } - in - queue_or_issue pgip - end + fun normalmsg area cat urgent s = + let + val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) + val pgip = Normalresponse {area=area,messagecategory=cat, + urgent=urgent,content=[content] } + in + queue_or_issue pgip + end fun errormsg fatality s = - let + let val content = XML.Elem("pgmltext",[],[XML.Rawtext s]) - val pgip = Errorresponse {area=NONE,fatality=fatality, - content=[content], - (* FIXME: pass in locations *) - location=NONE} - in - queue_or_issue pgip - end + val pgip = Errorresponse {area=NONE,fatality=fatality, + content=[content], + (* FIXME: pass in locations *) + location=NONE} + in + queue_or_issue pgip + end fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []) fun end_delayed_msgs () = (reset delay_msgs; ! delayed_msgs) @@ -199,7 +198,7 @@ (* NB: all of the standard error/message functions now expect already-escaped text. FIXME: this may cause us problems now we're generating trees; on the other - hand the output functions were tuned some time ago, so it ought to be + hand the output functions were tuned some time ago, so it ought to be enough to use Rawtext always above. *) fun setup_messages () = @@ -227,10 +226,10 @@ fun statedisplay prts = let - val display = Pretty.output (Pretty.chunks prts) - val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display]) + val display = Pretty.output (Pretty.chunks prts) + val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display]) in - issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]}) + issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]}) end fun print_current_goals n m st = @@ -245,7 +244,7 @@ (Display.print_current_goals_fn := print_current_goals; Toplevel.print_state_fn := print_state); (* Toplevel.prompt_state_fn := (fn s => suffix (special "372") - (Toplevel.prompt_state_default s))); *) + (Toplevel.prompt_state_default s))); *) end; @@ -327,12 +326,12 @@ val spaces_quote = space_implode " " o map quote; fun thm_deps_message (thms, deps) = - let - val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms]) - val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps]) + let + val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms]) + val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps]) in - issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")], - content=[valuethms,valuedeps]}) + issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")], + content=[valuethms,valuedeps]}) end (* FIXME: check this uses non-transitive closure function here *) @@ -356,14 +355,14 @@ (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **) -fun lexicalstructure_keywords () = +fun lexicalstructure_keywords () = let val commands = OuterSyntax.dest_keywords () - fun category_of k = if (k mem commands) then "major" else "minor" + 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.Elem("keyword", [("word", keyword), ("category", category_of kind)], - [XML.Elem("shorthelp", [], [XML.Text help])]) - in + fun keyword_elt (keyword,help,kind,_) = + XML.Elem("keyword", [("word", keyword), ("category", category_of kind)], + [XML.Elem("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 *) Lexicalstructure {content = map keyword_elt (OuterSyntax.dest_parsers()) } @@ -378,34 +377,34 @@ local val isabellewww = "http://isabelle.in.tum.de/" val staticconfig = "~~/lib/ProofGeneral/pgip_isar.xml" - fun orenv v d = case (getenv v) of "" => d | s => s + fun orenv v d = case getenv v of "" => d | s => s fun config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww in fun send_pgip_config () = let val path = Path.explode (config_file()) - val exists = File.exists path + val ex = File.exists path - val wwwpage = - (Url.explode (isabelle_www())) - handle _ => - (Output.panic - ("Error in URL in environment variable ISABELLE_HOMEPAGE."); - Url.explode isabellewww) - - val proverinfo = + val wwwpage = + (Url.explode (isabelle_www())) + handle _ => + (Output.panic + ("Error in URL in environment variable ISABELLE_HOMEPAGE."); + Url.explode isabellewww) + + val proverinfo = Proverinfo { name = "Isabelle", - version = version, - instance = Session.name(), - descr = "The Isabelle/Isar theorem prover", - url = wwwpage, - filenameextns = ".thy;" } + version = version, + instance = Session.name(), + descr = "The Isabelle/Isar theorem prover", + url = wwwpage, + filenameextns = ".thy;" } in - if exists then - (issue_pgip proverinfo; - issue_pgip_rawtext (File.read path); - issue_pgip (lexicalstructure_keywords())) + if ex then + (issue_pgip proverinfo; + issue_pgip_rawtext (File.read path); + issue_pgip (lexicalstructure_keywords())) else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found") end; end @@ -421,7 +420,7 @@ |> map #3 |> Toplevel.>>>; -(* TODO: +(* TODO: - apply a command given a transition function, e.g. IsarCmd.undo. - fix position from path of currently open file [line numbers risk garbling though]. *) @@ -433,8 +432,8 @@ 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))) + "" => 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 @@ -443,54 +442,54 @@ (******* PGIP actions *******) -(* Responses to each of the PGIP input commands. +(* Responses to each of the PGIP input commands. These are programmed uniformly for extensibility. *) -fun askpgip (Askpgip vs) = +fun askpgip (Askpgip vs) = issue_pgip (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported, - pgipelems = PgipIsabelle.accepted_inputs }) + pgipelems = PgipIsabelle.accepted_inputs }) -fun askpgml (Askpgml vs) = +fun askpgml (Askpgml vs) = issue_pgip - (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported }) + (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported }) fun askprefs (Askprefs vs) = - let - fun preference_of {name, descr, default, pgiptype, get, set } = - { name = name, descr = SOME descr, default = SOME default, - pgiptype = pgiptype } + let + fun preference_of {name, descr, default, pgiptype, get, set } = + { name = name, descr = SOME descr, default = SOME default, + pgiptype = pgiptype } in - List.app (fn (prefcat, prefs) => - issue_pgip (Hasprefs {prefcategory=SOME prefcat, - prefs=map preference_of prefs})) + List.app (fn (prefcat, prefs) => + issue_pgip (Hasprefs {prefcategory=SOME prefcat, + prefs=map preference_of prefs})) Preferences.preferences - end + end fun askconfig (Askconfig vs) = () (* TODO: add config response *) local - fun lookuppref pref = - case AList.lookup (op =) - (map (fn p => (#name p,p)) - (maps snd Preferences.preferences)) pref of - NONE => error ("Unknown prover preference: " ^ quote pref) - | SOME p => p + fun lookuppref pref = + case AList.lookup (op =) + (map (fn p => (#name p,p)) + (maps snd Preferences.preferences)) pref of + NONE => error ("Unknown prover preference: " ^ quote pref) + | SOME p => p in -fun setpref (Setpref vs) = - let - val name = #name vs - val value = #value vs - val set = #set (lookuppref name) +fun setpref (Setpref vs) = + let + val name = #name vs + val value = #value vs + val set = #set (lookuppref name) in - set value + set value end fun getpref (Getpref vs) = - let - val name = #name vs - val get = #get (lookuppref name) - in + let + val name = #name vs + val get = #get (lookuppref name) + in issue_pgip (Prefval {name=name, value=get ()}) end end @@ -503,30 +502,30 @@ fun stopquiet vs = isarcmd "enable_pr" -fun pgmlsymbolson vs = +fun pgmlsymbolson vs = change print_mode (fn mode => - remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN]) + remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN]) fun pgmlsymbolsoff vs = change print_mode (remove (op =) Symbol.xsymbolsN) -fun dostep (Dostep vs) = - let - val text = #text vs - in - isarcmd text +fun dostep (Dostep vs) = + let + val text = #text vs + in + isarcmd text end fun undostep (Undostep vs) = - let - val times = #times vs - in - isarcmd ("undos_proof " ^ (Int.toString times)) + let + val times = #times vs + in + isarcmd ("undos_proof " ^ Int.toString times) end fun redostep vs = isarcmd "redo" - -fun abortgoal vs = isarcmd "ProofGeneral.kill_proof" + +fun abortgoal vs = isarcmd "ProofGeneral.kill_proof" (*** PGIP identifier tables ***) @@ -536,126 +535,126 @@ fun delids t = issue_pgip (Delids {idtables = [t]}) (* - fun delallids ty = - issue_pgip (Setids {idtables = - [{context=NONE,objtype=ty,ids=[]}]}) *) + fun delallids ty = + issue_pgip (Setids {idtables = + [{context=NONE,objtype=ty,ids=[]}]}) *) -fun askids (Askids vs) = +fun askids (Askids vs) = let - val url = #url vs (* ask for identifiers within a file *) - val thyname = #thyname vs (* ask for identifiers within a theory *) - val objtype = #objtype vs (* ask for identifiers of a particular type *) + val url = #url vs (* ask for identifiers within a file *) + val thyname = #thyname vs (* ask for identifiers within a theory *) + val objtype = #objtype vs (* ask for identifiers of a particular type *) - fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} + fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids} - val thms_of_thy = (map fst) o PureThy.thms_of o ThyInfo.get_theory - in -(* case (url_attr,thyname,objtype) of - (NONE,NONE,NONE) => -*) (* top-level: return *) + val thms_of_thy = map fst o PureThy.thms_of o ThyInfo.get_theory + in +(* case (url_attr,thyname,objtype) of + (NONE,NONE,NONE) => +*) (* top-level: return *) - (* TODO: add askids for "file" here, which returns single theory with same name *) + (* TODO: add askids for "file" here, which returns single theory with same name *) (* FIXME: objtypes on both sides *) - case (thyname,objtype) of + case (thyname,objtype) of (* only files known in top context *) - (NONE, NONE) => setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris?*) - | (NONE, SOME ObjFile) => setids (idtable ObjFile NONE (ThyInfo.names())) (* ditto *) - | (SOME fi, SOME ObjFile) => setids (idtable ObjTheory (SOME fi) [fi]) (* FIXME: lookup file *) - | (NONE, SOME ObjTheory) => setids (idtable ObjTheory NONE (ThyInfo.names())) - | (SOME thy, SOME ObjTheory) => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy)) - | (SOME thy, SOME ObjTheorem) => setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy)) - (* next case is both of above. FIXME: cleanup this *) - | (SOME thy, NONE) => (setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy)); - setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy))) - | (_, SOME ot) => error ("No objects of type "^(PgipTypes.name_of_objtype ot)^" are available here.") + (NONE, NONE) => setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris?*) + | (NONE, SOME ObjFile) => setids (idtable ObjFile NONE (ThyInfo.names())) (* ditto *) + | (SOME fi, SOME ObjFile) => setids (idtable ObjTheory (SOME fi) [fi]) (* FIXME: lookup file *) + | (NONE, SOME ObjTheory) => setids (idtable ObjTheory NONE (ThyInfo.names())) + | (SOME thy, SOME ObjTheory) => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy)) + | (SOME thy, SOME ObjTheorem) => setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy)) + (* next case is both of above. FIXME: cleanup this *) + | (SOME thy, NONE) => (setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy)); + setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy))) + | (_, SOME ot) => error ("No objects of type "^(PgipTypes.name_of_objtype ot)^" are available here.") end local (* accumulate printed output in a single PGIP response (inside ) *) fun with_displaywrap pgipfn dispfn = let - val lines = ref ([]: string list); - fun wlgrablines s = lines := s :: ! lines; + val lines = ref ([]: string list); + fun wlgrablines s = lines := s :: ! lines; in - setmp writeln_fn wlgrablines dispfn (); - issue_pgip (pgipfn (!lines)) + setmp writeln_fn wlgrablines dispfn (); + issue_pgip (pgipfn (!lines)) end; in -fun showid (Showid vs) = +fun showid (Showid vs) = let - val thyname = #thyname vs - val objtype = #objtype vs - val name = #name vs - val topthy = Toplevel.theory_of o Toplevel.get_state + val thyname = #thyname vs + val objtype = #objtype vs + val name = #name vs + val topthy = Toplevel.theory_of o Toplevel.get_state - fun idvalue objtype name strings = - Idvalue { name=name, objtype=objtype, - text=[XML.Elem("pgmltext",[],map XML.Text strings)] } + fun idvalue objtype name strings = + Idvalue { name=name, objtype=objtype, + text=[XML.Elem("pgmltext",[],map XML.Text strings)] } - fun pthm thy name = print_thm (get_thm thy (Name name)) - in - case (thyname, objtype) of - (_,ObjTheory) => - with_displaywrap (idvalue ObjTheory name) - (fn ()=>(print_theory (ThyInfo.get_theory name))) - | (SOME thy, ObjTheorem) => - with_displaywrap (idvalue ObjTheorem name) - (fn ()=>(pthm (ThyInfo.get_theory thy) name)) - | (NONE, ObjTheorem) => - with_displaywrap (idvalue ObjTheorem name) - (fn ()=>pthm (topthy()) name) - | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot)) + fun pthm thy name = print_thm (get_thm thy (Name name)) + in + case (thyname, objtype) of + (_,ObjTheory) => + with_displaywrap (idvalue ObjTheory name) + (fn ()=>(print_theory (ThyInfo.get_theory name))) + | (SOME thy, ObjTheorem) => + with_displaywrap (idvalue ObjTheorem name) + (fn ()=>(pthm (ThyInfo.get_theory thy) name)) + | (NONE, ObjTheorem) => + with_displaywrap (idvalue ObjTheorem name) + (fn ()=>pthm (topthy()) name) + | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot)) end (*** Inspecting state ***) -(* The file which is currently being processed interactively. +(* The file which is currently being processed interactively. In the pre-PGIP code, this was informed to Isabelle and the theory loader on completion, but that allows for circularity in case we read ourselves. So PGIP opens the filename at the start of a script. We ought to prevent problems by modifying the theory loader to know - about this special status, but for now we just keep a local reference. -*) + about this special status, but for now we just keep a local reference. +*) val currently_open_file = ref (NONE : pgipurl option) -fun askguise vs = +fun askguise vs = (* The "guise" is the PGIP abstraction of the prover's state. The message is merely used for consistency checking. *) - let - val openfile = !currently_open_file + let + val openfile = !currently_open_file - val topthy = Toplevel.theory_of o Toplevel.get_state - val topthy_name = Context.theory_name o topthy + val topthy = Toplevel.theory_of o Toplevel.get_state + val topthy_name = Context.theory_name o topthy - val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE + val opentheory = SOME (topthy_name()) handle Toplevel.UNDEF => NONE - fun topproofpos () = try Toplevel.proof_position_of (Isar.state ()); - val openproofpos = topproofpos() + fun topproofpos () = try Toplevel.proof_position_of (Isar.state ()); + val openproofpos = topproofpos() in issue_pgip (Informguise { file = openfile, - theory = opentheory, - (* would be nice to get thm name... *) - theorem = NONE, - proofpos = openproofpos }) + theory = opentheory, + (* would be nice to get thm name... *) + theorem = NONE, + proofpos = openproofpos }) end fun parsescript (Parsescript vs) = let - val text = #text vs - val systemdata = #systemdata vs - val location = #location vs (* TODO: extract position *) + val text = #text vs + val systemdata = #systemdata vs + val location = #location vs (* TODO: extract position *) val _ = start_delay_msgs () (* gather parsing errs/warns *) val doc = PgipParser.pgip_parser text val errs = end_delayed_msgs () - val sysattrs = PgipTypes.opt_attr "systemdata" systemdata - val locattrs = PgipTypes.attrs_of_location location + val sysattrs = PgipTypes.opt_attr "systemdata" systemdata + val locattrs = PgipTypes.attrs_of_location location in issue_pgip (Parseresult { attrs= sysattrs@locattrs, - doc = doc, - errs = (map PgipOutput.output errs) }) + doc = doc, + errs = map PgipOutput.output errs }) end fun showproofstate vs = isarcmd "pr" @@ -663,33 +662,33 @@ fun showctxt vs = isarcmd "print_theory" (* more useful than print_context *) fun searchtheorems (Searchtheorems vs) = - let - val arg = #arg vs + let + val arg = #arg vs in - isarcmd ("thms_containing " ^ arg) + isarcmd ("thms_containing " ^ arg) end -fun setlinewidth (Setlinewidth vs) = - let - val width = #width vs +fun setlinewidth (Setlinewidth vs) = + let + val width = #width vs in - isarcmd ("pretty_setmargin " ^ (Int.toString width)) (* FIXME: conversion back/forth! *) + isarcmd ("pretty_setmargin " ^ Int.toString width) (* FIXME: conversion back/forth! *) end fun viewdoc (Viewdoc vs) = - let - val arg = #arg vs - in - isarcmd ("print_" ^ arg) (* FIXME: isatool doc?. Return URLs, maybe? *) + let + val arg = #arg vs + in + isarcmd ("print_" ^ arg) (* FIXME: isatool doc?. Return URLs, maybe? *) end (*** Theory ***) fun doitem (Doitem vs) = let - val text = #text vs + val text = #text vs in - isarcmd text + isarcmd text end fun undoitem vs = @@ -698,14 +697,14 @@ fun redoitem vs = isarcmd "ProofGeneral.redo" -fun aborttheory vs = +fun aborttheory vs = isarcmd "init_toplevel" fun retracttheory (Retracttheory vs) = - let - val thyname = #thyname vs + let + val thyname = #thyname vs in - isarcmd ("kill_thy " ^ quote thyname) + isarcmd ("kill_thy " ^ quote thyname) end @@ -715,16 +714,16 @@ 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 assume that the prover has a load path. + NB: PGIP does not assume that the prover has a load path. *) local val current_working_dir = ref (NONE : string option) in -fun changecwd_dir newdirpath = - let +fun changecwd_dir newdirpath = + let val newdir = File.platform_path newdirpath - in + in (case (!current_working_dir) of NONE => () | SOME dir => ThyLoad.del_path dir; @@ -733,16 +732,16 @@ end end -fun changecwd (Changecwd vs) = - let - val url = #url vs - val newdir = PgipTypes.path_of_pgipurl url +fun changecwd (Changecwd vs) = + let + val url = #url vs + val newdir = PgipTypes.path_of_pgipurl url in - changecwd_dir url + changecwd_dir url end fun openfile (Openfile vs) = - let + let val url = #url vs val filepath = PgipTypes.path_of_pgipurl url val filedir = Path.dir filepath @@ -752,22 +751,22 @@ case !currently_open_file of SOME f => raise PGIP (" when a file is already open! ") | NONE => (openfile_retract filepath; - changecwd_dir filedir; - currently_open_file := SOME url) + changecwd_dir filedir; + currently_open_file := SOME url) end fun closefile vs = case !currently_open_file of - SOME f => (proper_inform_file_processed (File.platform_path f) - (Isar.state()); + SOME f => (proper_inform_file_processed (File.platform_path f) + (Isar.state()); currently_open_file := NONE) | NONE => raise PGIP (" when no file is open!") -fun loadfile (Loadfile vs) = - let - val url = #url vs - in - case !currently_open_file of +fun loadfile (Loadfile vs) = + let + val url = #url vs + in + case !currently_open_file of SOME f => raise PGIP (" when a file is open!") | NONE => use_thy_or_ml_file (File.platform_path url) end @@ -775,14 +774,14 @@ fun abortfile vs = case !currently_open_file of SOME f => (isarcmd "init_toplevel"; - currently_open_file := NONE) + currently_open_file := NONE) | NONE => raise PGIP (" when no file is open!") -fun retractfile (Retractfile vs) = - let - val url = #url vs +fun retractfile (Retractfile vs) = + let + val url = #url vs in - case !currently_open_file of + case !currently_open_file of SOME f => raise PGIP (" when a file is open!") | NONE => inform_file_retracted (File.platform_path url) end @@ -791,7 +790,7 @@ (*** System ***) fun systemcmd (Systemcmd vs) = - let + let val arg = #arg vs in isarcmd arg @@ -803,7 +802,7 @@ fun process_input inp = case inp of Pgip.Askpgip _ => askpgip inp | Pgip.Askpgml _ => askpgml inp - | Pgip.Askprefs _ => askprefs inp + | Pgip.Askprefs _ => askprefs inp | Pgip.Askconfig _ => askconfig inp | Pgip.Getpref _ => getpref inp | Pgip.Setpref _ => setpref inp @@ -843,18 +842,18 @@ | Pgip.Quitpgip _ => quitpgip inp -fun process_pgip_element pgipxml = +fun process_pgip_element pgipxml = case pgipxml of - (xml as (XML.Elem elem)) => - (case Pgip.input elem of - NONE => warning ("Unrecognized PGIP command, ignored: \n" ^ - (XML.string_of_tree xml)) - | SOME inp => (process_input inp)) (* errors later; packet discarded *) + (xml as (XML.Elem elem)) => + (case Pgip.input elem of + NONE => warning ("Unrecognized PGIP command, ignored: \n" ^ + (XML.string_of_tree xml)) + | SOME inp => (process_input inp)) (* errors later; packet discarded *) | (XML.Text t) => ignored_text_warning t - | (XML.Rawtext t) => ignored_text_warning t + | (XML.Rawtext t) => ignored_text_warning t and ignored_text_warning t = - if (size (Symbol.strip_blanks t) > 0) then - warning ("Ignored text in PGIP packet: \n" ^ t) + if size (Symbol.strip_blanks t) > 0 then + warning ("Ignored text in PGIP packet: \n" ^ t) else () fun process_pgip_tree xml = @@ -865,27 +864,27 @@ (let val class = PgipTypes.get_attr "class" attrs val dest = PgipTypes.get_attr_opt "destid" attrs - val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs) + val seq = PgipTypes.read_pgipnat (PgipTypes.get_attr "seq" attrs) (* Respond to prover broadcasts, or messages for us. Ignore rest *) - val processit = - case dest of + val processit = + case dest of NONE => class = "pa" - | SOME id => matching_pgip_id id - in if processit then - (pgip_refid := PgipTypes.get_attr_opt "id" attrs; - pgip_refseq := SOME seq; - List.app process_pgip_element pgips; - (* return true to indicate *) - true) - else - (* no response to ignored messages. *) - false + | SOME id => matching_pgip_id id + in if processit then + (pgip_refid := PgipTypes.get_attr_opt "id" attrs; + pgip_refseq := SOME seq; + List.app process_pgip_element pgips; + (* return true to indicate *) + true) + else + (* no response to ignored messages. *) + false end) | _ => raise PGIP "Invalid PGIP packet received") handle PGIP msg => (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^ - (XML.string_of_tree xml)); - true)) + (XML.string_of_tree xml)); + true)) (* External input *) @@ -910,8 +909,8 @@ NONE => () | SOME (pgip,src') => let - val ready' = (process_pgip_tree pgip) - handle e => (handler (e,SOME src'); true) + val ready' = (process_pgip_tree pgip) + handle e => (handler (e,SOME src'); true) in loop ready' src' end @@ -922,12 +921,12 @@ (XML_PARSE,SOME src) => Output.panic "Invalid XML input, aborting" | (PGIP_QUIT,_) => () - | (Interrupt,SOME src) => - (Output.error_msg "Interrupt during PGIP processing"; loop true src) - | (Toplevel.UNDEF,SOME src) => - (Output.error_msg "No working context defined"; loop true src) - | (e,SOME src) => - (Output.error_msg (Toplevel.exn_message e); loop true src) + | (Interrupt,SOME src) => + (Output.error_msg "Interrupt during PGIP processing"; loop true src) + | (Toplevel.UNDEF,SOME src) => + (Output.error_msg "No working context defined"; loop true src) + | (e,SOME src) => + (Output.error_msg (Toplevel.exn_message e); loop true src) | (_,NONE) => () in (* TODO: add socket interface *) @@ -940,7 +939,7 @@ end -(* additional outer syntax for Isar *) +(* additional outer syntax for Isar *) (* da: TODO: perhaps we can drop this superfluous syntax now?? Seems cleaner to support the operations directly above in the PGIP actions. *) @@ -1033,11 +1032,11 @@ (* Set recipient for PGIP results *) fun init_pgip_channel writefn = - (init_pgip_session_id(); - pgip_output_channel := writefn) + (init_pgip_session_id(); + pgip_output_channel := writefn) -(* Process a PGIP command. - This works for preferences but not generally guaranteed +(* Process a PGIP command. + This works for preferences but not generally guaranteed because we haven't done full setup here (e.g., no pgml mode) *) fun process_pgip str = setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str diff -r 9b772ac66830 -r fbd068dd4d29 src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Fri Dec 29 18:25:45 2006 +0100 +++ b/src/Pure/proof_general.ML Fri Dec 29 18:25:46 2006 +0100 @@ -53,7 +53,6 @@ val proof_generalN = "ProofGeneral"; (*token markup (colouring vars, etc.)*) val pgasciiN = "PGASCII"; (*plain 7-bit ASCII communication*) -val xsymbolsN = Symbol.xsymbolsN; (*X-Symbol 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*) @@ -73,7 +72,7 @@ | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s; fun xsymbols_output s = - if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then + 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; @@ -94,7 +93,7 @@ in fun setup_xsymbols_output () = - Output.add_mode xsymbolsN + Output.add_mode Symbol.xsymbolsN (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw); fun setup_pgml_output () = @@ -314,20 +313,20 @@ fun tell_file_loaded path = if pgip () then issue_pgipe "informfileloaded" - [localfile_url_attr (XML.text (File.platform_path - (File.full_path path)))] + [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)); + 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)))] + [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)); + emacs_notify ("Proof General, you can unlock the file " + ^ quote (File.platform_path path)); (* theory / proof state output *) @@ -618,21 +617,21 @@ ("Track theorem dependencies within Proof General", thm_deps_option)), ("skip-proofs", - ("Ignore proof scripts (interactive-only)", + ("Skip over proofs (interactive-only)", bool_option Toplevel.skip_proofs))]) ]; end; (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **) -fun lexicalstructure_keywords () = +fun lexicalstructure_keywords () = let val commands = OuterSyntax.dest_keywords () - fun category_of k = if (k mem commands) then "major" else "minor" + 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 + 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())) @@ -657,18 +656,18 @@ 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;")] + [("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()]) + (issue_pgips [proverinfo]; + issue_pgips [File.read path]; + issue_pgips [lexicalstructure_keywords()]) else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found") end; end @@ -1257,8 +1256,8 @@ | "closegoal" => isarscript data | "giveupgoal" => isarscript data | "postponegoal" => isarscript data - | "comment" => isarscript data - | "doccomment" => 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 @@ -1303,14 +1302,14 @@ | "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))) + 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) + 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!")