Revamped Proof General interface.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/README Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,36 @@
+Proof General interface for Isabelle.
+
+This includes a prover-side PGIP abstraction layer for passing
+interface configuration, control commands and display messages to
+Proof General.
+
+ pgip_types.ML -- the datatypes in PGIP and their manipulation
+ pgip_input.ML -- commands sent to the prover
+ pgip_output.ML -- commands the prover sends out
+ pgip_markup.ML -- markup for proof script documents
+ pgip.ML -- union of the above
+ pgip_tests.ML -- some basic testing of the API
+
+The code constructs some marshalling datatypes for reading and writing
+XML which conforms to the PGIP schema, interfacing with SML types and
+some basic types from the Isabelle platform (i.e. URLs, XML). This
+part of the code is intended to be useful for reuse or porting
+elsewhere, so it should have minimal dependency on Isabelle and be
+written readably. Some languages have tools for making type-safe
+XML<->native datatype translations from a schema (e.g. HaXML for
+Haskell) which would be useful here.
+
+The Isabelle specific configuration is in these files:
+
+ pgip_isabelle.ML - configure part of PGIP supported by Isabelle
+ parsing.ML - parsing routines to add PGIP markup to scripts
+ preferences.ML - user preferences
+ proof_general_pgip.ML - the main connection point with Isabelle, including
+ the PGIP processing loop.
+
+For the full PGIP schema and an explanation of it, see:
+
+ http://proofgeneral.inf.ed.ac.uk/kit
+
+David Aspinall, Dec. 2006.
+$Id$
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/ROOT.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,15 @@
+use "pgip_types.ML";
+use "pgip_markup.ML";
+use "pgip_input.ML";
+use "pgip_output.ML";
+use "pgip.ML";
+use "pgip_tests.ML";
+
+use "pgip_isabelle.ML";
+use "preferences.ML";
+use "parsing.ML";
+
+(use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_pgip.ML";
+(* OLD interaction mode, not yet complete
+ (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_emacs.ML";
+*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/parsing.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,339 @@
+(* Title: Pure/ProofGeneral/parsing.ML
+ ID: $Id$
+ Author: David Aspinall
+
+Parsing theory files to add PGIP markup.
+*)
+
+signature PGIP_PARSER =
+sig
+ val xmls_of_str: string -> XML.tree list
+end
+
+structure PgipParser : PGIP_PARSER =
+struct
+
+
+(** Parsing proof scripts without execution **)
+
+structure P = OuterParse;
+
+(* 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.Elem(elt, [], [XML.Text str])]
+ fun markup_text_attrs str elt attrs = [XML.Elem(elt, attrs, [XML.Text str])]
+ fun empty elt = [XML.Elem(elt, [], [])]
+
+ fun whitespace str = XML.Elem("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.Elem(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
+end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgip.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,22 @@
+(* Title: Pure/ProofGeneral/pgip.ML
+ ID: $Id$
+ Author: David Aspinall
+
+Prover-side PGIP abstraction.
+Not too closely tied to Isabelle, to help with reuse/porting.
+*)
+
+signature PGIP =
+sig
+ include PGIPTYPES
+ include PGIPINPUT
+ include PGIPOUTPUT
+end
+
+structure Pgip : PGIP =
+struct
+ open PgipTypes
+ open PgipInput
+ open PgipOutput
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgip_input.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,216 @@
+(* Title: Pure/ProofGeneral/pgip_input.ML
+ ID: $Id$
+ Author: David Aspinall
+
+PGIP abstraction: input commands
+*)
+
+signature PGIPINPUT =
+sig
+ (* These are the PGIP commands to which we respond. *)
+ datatype pgipinput =
+ (* protocol/prover config *)
+ Askpgip of { }
+ | Askpgml of { }
+ | Askconfig of { }
+ | Askprefs of { }
+ | Setpref of { name:string, prefcategory:string option, value:string }
+ | Getpref of { name:string, prefcategory:string option }
+ (* prover control *)
+ | Proverinit of { }
+ | Proverexit of { }
+ | Startquiet of { }
+ | Stopquiet of { }
+ | Pgmlsymbolson of { }
+ | Pgmlsymbolsoff of { }
+ (* improper proof commands: control proof state *)
+ | Dostep of { text: string }
+ | Undostep of { times: int }
+ | Redostep of { }
+ | Abortgoal of { }
+ | Forget of { thyname: string option, name: string option,
+ objtype: string option }
+ | Restoregoal of { thmname : string }
+ (* context inspection commands *)
+ | Askids of { thyname:string option, objtype:string option }
+ | Showid of { thyname:string option, objtype:string, name:string }
+ | Askguise of { }
+ | Parsescript of { text: string, location: PgipTypes.location,
+ systemdata: string option }
+ | Showproofstate of { }
+ | Showctxt of { }
+ | Searchtheorems of { arg: string }
+ | Setlinewidth of { width: int }
+ | Viewdoc of { arg: string }
+ (* improper theory-level commands *)
+ | Doitem of { text: string }
+ | Undoitem of { }
+ | Redoitem of { }
+ | Aborttheory of { }
+ | Retracttheory of { thyname: string }
+ | Loadfile of { url: PgipTypes.pgipurl }
+ | Openfile of { url: PgipTypes.pgipurl }
+ | Closefile of { }
+ | Abortfile of { }
+ | Retractfile of { url: PgipTypes.pgipurl }
+ | Changecwd of { url: PgipTypes.pgipurl }
+ | Systemcmd of { arg: string }
+ (* unofficial escape command for debugging *)
+ | Quitpgip of { }
+
+ val input : XML.element -> pgipinput option (* raises PGIP *)
+end
+
+structure PgipInput : PGIPINPUT =
+struct
+
+open PgipTypes
+
+(*** PGIP input ***)
+
+datatype pgipinput =
+ (* protocol/prover config *)
+ Askpgip of { }
+ | Askpgml of { }
+ | Askconfig of { }
+ | Askprefs of { }
+ | Setpref of { name:string, prefcategory:string option, value:string }
+ | Getpref of { name:string, prefcategory:string option }
+ (* prover control *)
+ | Proverinit of { }
+ | Proverexit of { }
+ | Startquiet of { }
+ | Stopquiet of { }
+ | Pgmlsymbolson of { }
+ | Pgmlsymbolsoff of { }
+ (* improper proof commands: control proof state *)
+ | Dostep of { text: string }
+ | Undostep of { times: int }
+ | Redostep of { }
+ | Abortgoal of { }
+ | Forget of { thyname: string option, name: string option,
+ objtype: string option }
+ | Restoregoal of { thmname : string }
+ (* context inspection commands *)
+ | Askids of { thyname:string option, objtype:string option }
+ | Showid of { thyname:string option, objtype:string, name:string }
+ | Askguise of { }
+ | Parsescript of { text: string, location: location,
+ systemdata: string option }
+ | Showproofstate of { }
+ | Showctxt of { }
+ | Searchtheorems of { arg: string }
+ | Setlinewidth of { width: int }
+ | Viewdoc of { arg: string }
+ (* improper theory-level commands *)
+ | Doitem of { text: string }
+ | Undoitem of { }
+ | Redoitem of { }
+ | Aborttheory of { }
+ | Retracttheory of { thyname: string }
+ | Loadfile of { url: pgipurl }
+ | Openfile of { url: pgipurl }
+ | Closefile of { }
+ | Abortfile of { }
+ | Retractfile of { url: pgipurl }
+ | Changecwd of { url: pgipurl }
+ | Systemcmd of { arg: string }
+ (* unofficial escape command for debugging *)
+ | Quitpgip of { }
+
+(* Extracting content from input XML elements to make a PGIPinput *)
+local
+
+ val thyname_attro = get_attr_opt "thyname"
+ val thyname_attr = get_attr "thyname"
+ val objtype_attro = get_attr_opt "objtype"
+ val objtype_attr = get_attr "objtype"
+ val name_attr = get_attr "name"
+ val name_attro = get_attr_opt "name"
+ val thmname_attr = get_attr "thmname"
+
+ 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)
+ | xmltext [] = ""
+ | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
+
+ exception Unknown
+ exception NoAction
+in
+
+(* Return a valid PGIP input command.
+ Raise PGIP exception for invalid data.
+ Return NONE for unknown/unhandled commands.
+*)
+fun input (elem, attrs, data) =
+SOME
+ (case elem of
+ "askpgip" => Askpgip { }
+ | "askpgml" => Askpgml { }
+ | "askconfig" => Askconfig { }
+ (* proverconfig *)
+ | "askprefs" => Askprefs { }
+ | "getpref" => Getpref { name = name_attr attrs,
+ prefcategory = prefcat_attr attrs }
+ | "setpref" => Setpref { name = name_attr attrs,
+ prefcategory = prefcat_attr attrs,
+ value = xmltext data }
+ (* provercontrol *)
+ | "proverinit" => Proverinit { }
+ | "proverexit" => Proverexit { }
+ | "startquiet" => Startquiet { }
+ | "stopquiet" => Stopquiet { }
+ | "pgmlsymbolson" => Pgmlsymbolson { }
+ (* improperproofcmd: improper commands not in script *)
+ | "dostep" => Dostep { text = xmltext data }
+ | "undostep" => Undostep { times = times_attr attrs }
+ | "redostep" => Redostep { }
+ | "abortgoal" => Abortgoal { }
+ | "forget" => Forget { thyname = thyname_attro attrs,
+ name = name_attro attrs,
+ objtype = objtype_attro attrs }
+ | "restoregoal" => Restoregoal { thmname = thmname_attr attrs}
+ (* proofctxt: improper commands *)
+ | "askids" => Askids { thyname = thyname_attro attrs,
+ objtype = objtype_attro attrs }
+ | "showid" => Showid { thyname = thyname_attro attrs,
+ objtype = objtype_attr attrs,
+ name = name_attr attrs }
+ | "askguise" => Askguise { }
+ | "parsescript" => Parsescript { text = (xmltext data),
+ systemdata = get_attr_opt "systemdata" attrs,
+ location = location_of_attrs attrs }
+ | "showproofstate" => Showproofstate { }
+ | "showctxt" => Showctxt { }
+ | "searchtheorems" => Searchtheorems { arg = xmltext data }
+ | "setlinewidth" => Setlinewidth { width = read_pgipnat (xmltext data) }
+ | "viewdoc" => Viewdoc { arg = xmltext data }
+ (* improperfilecmd: theory-level commands not in script *)
+ | "doitem" => Doitem { text = xmltext data }
+ | "undoitem" => Undoitem { }
+ | "redoitem" => Redoitem { }
+ | "aborttheory" => Aborttheory { }
+ | "retracttheory" => Retracttheory { thyname = thyname_attr attrs }
+ | "loadfile" => Loadfile { url = pgipurl_of_attrs attrs }
+ | "openfile" => Openfile { url = pgipurl_of_attrs attrs }
+ | "closefile" => Closefile { }
+ | "abortfile" => Abortfile { }
+ | "retractfile" => Retractfile { url = pgipurl_of_attrs attrs }
+ | "changecwd" => Changecwd { url = pgipurl_of_attrs attrs }
+ | "systemcmd" => Systemcmd { arg = xmltext data }
+ (* unofficial command for debugging *)
+ | "quitpgip" => Quitpgip { }
+
+ (* We allow sending proper document markup too; we map it back to dostep *)
+ (* and strip out metainfo elements. Markup correctness isn't checked: this *)
+ (* is a compatibility measure to make it easy for interfaces. *)
+ | "metainfo" => raise NoAction
+ | x => if (x mem PgipMarkup.markup_elements)
+ then Dostep { text = xmltext data } (* could use Doitem too *)
+ else raise Unknown)
+ handle Unknown => NONE | NoAction => NONE
+end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,58 @@
+(* Title: Pure/ProofGeneral/pgip_isabelle.ML
+ ID: $Id$
+ Author: David Aspinall
+
+Prover-side PGIP abstraction: Isabelle configuration
+*)
+
+signature PGIP_ISABELLE =
+sig
+ val isabelle_pgml_version_supported : string
+ val isabelle_pgip_version_supported : string
+ val accepted_inputs : (string * bool * (string list)) list
+end
+
+structure PgipIsabelle : PGIP_ISABELLE =
+struct
+
+val isabelle_pgml_version_supported = "1.0";
+val isabelle_pgip_version_supported = "2.0"
+
+(** Accepted commands **)
+
+local
+
+ (* These element names are a subset of those in pgip_input.ML.
+ They must be handled in proof_general_pgip.ML/process_pgip_element. *)
+
+ val accepted_names =
+ (* not implemented: "askconfig", "forget", "restoregoal" *)
+ ["askpgip","askpgml","askprefs","getpref","setpref",
+ "proverinit","proverexit","startquiet","stopquiet",
+ "pgmlsymbolson", "pgmlsymbolsoff",
+ "dostep", "undostep", "redostep", "abortgoal",
+ "askids", "showid", "askguise",
+ "parsescript",
+ "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
+ "doitem", "undoitem", "redoitem", "abortheory",
+ "retracttheory", "loadfile", "openfile", "closefile",
+ "abortfile", "retractfile", "changecwd", "systemcmd"];
+
+ fun element_async p =
+ false (* single threaded only *)
+
+ fun supported_optional_attrs p = (case p of
+ "undostep" => ["times"]
+ (* TODO: we could probably extend these too:
+ | "redostep" => ["times"]
+ | "undoitem" => ["times"]
+ | "redoitem" => ["times"] *)
+ | _ => [])
+in
+val accepted_inputs =
+ (map (fn p=> (p, element_async p, supported_optional_attrs p))
+ accepted_names);
+end
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgip_markup.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,33 @@
+(* Title: Pure/ProofGeneral/pgip_markup.ML
+ ID: $Id$
+ Author: David Aspinall
+
+PGIP abstraction: document markup for proof scripts (in progress).
+*)
+
+signature PGIPMARKUP =
+sig
+ val markup_elements : string list
+end
+
+structure PgipMarkup : PGIPMARKUP =
+struct
+ (* Names of all PGIP document markup elements *)
+ val markup_elements =
+ [
+ "opengoal",
+ "proofstep",
+ "closegoal",
+ "comment",
+ "doccomment",
+ "whitespace",
+ "litcomment",
+ "spuriouscmd",
+ "badcmd",
+ "opentheory",
+ "theoryitem",
+ "closetheory",
+ "metainfo" (* non-document text *)
+ ]
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgip_output.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,366 @@
+(* Title: Pure/ProofGeneral/pgip_output.ML
+ ID: $Id$
+ Author: David Aspinall
+
+PGIP abstraction: output commands
+*)
+
+signature PGIPOUTPUT =
+sig
+ (* These are the PGIP messages which the prover emits. *)
+ datatype pgipoutput =
+ Cleardisplay of { area: PgipTypes.displayarea }
+ | Normalresponse of { area: PgipTypes.displayarea,
+ urgent: bool,
+ messagecategory: PgipTypes.messagecategory,
+ content: XML.tree list }
+ | Errorresponse of { fatality: PgipTypes.fatality,
+ area: PgipTypes.displayarea option,
+ location: PgipTypes.location option,
+ content: XML.tree list }
+ | Informfileloaded of { url: PgipTypes.pgipurl }
+ | Informfileretracted of { url: PgipTypes.pgipurl }
+ | Proofstate of { pgml: XML.tree list }
+ | Metainforesponse of { attrs: XML.attributes,
+ content: XML.tree list }
+ | Lexicalstructure of { content: XML.tree list }
+ | Proverinfo of { name: string,
+ version: string,
+ instance: string,
+ descr: string,
+ url: Url.T,
+ filenameextns: string }
+ | Idtable of { objtype: string,
+ context: string option,
+ ids: string list }
+ | Setids of { idtables: XML.tree list }
+ | Delids of { idtables: XML.tree list }
+ | Addids of { idtables: XML.tree list }
+ | Hasprefs of { prefcategory: string option,
+ prefs: PgipTypes.preference list }
+ | Prefval of { name: string, value: string }
+ | Idvalue of { name: string, objtype: string, text: XML.tree list }
+ | Informguise of { file : PgipTypes.pgipurl option,
+ theory: string option,
+ theorem: string option,
+ proofpos: int option }
+ | Parseresult of { attrs: XML.attributes, content: XML.tree list }
+ | Usespgip of { version: string,
+ pgipelems: (string * bool * string list) list }
+ | Usespgml of { version: string }
+ | Pgip of { tag: string option,
+ class: string,
+ seq: int, id: string,
+ destid: string option,
+ refid: string option,
+ refseq: int option,
+ content: XML.tree list }
+ | Ready of { }
+
+ val output : pgipoutput -> XML.tree
+end
+
+structure PgipOutput : PGIPOUTPUT =
+struct
+open PgipTypes
+
+datatype pgipoutput =
+ Cleardisplay of { area: displayarea }
+ | Normalresponse of { area: displayarea, urgent: bool,
+ messagecategory: messagecategory, content: XML.tree list }
+ | Errorresponse of { area: displayarea option, fatality: fatality,
+ location: location option, content: XML.tree list }
+ | Informfileloaded of { url: Path.T }
+ | Informfileretracted of { url: Path.T }
+ | Proofstate of { pgml: XML.tree list }
+ | Metainforesponse of { attrs: XML.attributes, content: XML.tree list }
+ | Lexicalstructure of { content: XML.tree list }
+ | Proverinfo of { name: string, version: string, instance: string,
+ descr: string, url: Url.T, filenameextns: string }
+ | Idtable of { objtype: string, context: string option, ids: string list }
+ | Setids of { idtables: XML.tree list }
+ | Delids of { idtables: XML.tree list }
+ | Addids of { idtables: XML.tree list }
+ | Hasprefs of { prefcategory: string option, prefs: preference list }
+ | Prefval of { name: string, value: string }
+ | Idvalue of { name: string, objtype: string, text: XML.tree list }
+ | Informguise of { file : pgipurl option, theory: string option,
+ theorem: string option, proofpos: int option }
+ | Parseresult of { attrs: XML.attributes, content: XML.tree list }
+ | Usespgip of { version: string,
+ pgipelems: (string * bool * string list) list }
+ | Usespgml of { version: string }
+ | Pgip of { tag: string option,
+ class: string,
+ seq: int, id: string,
+ destid: string option,
+ refid: string option,
+ refseq: int option,
+ content: XML.tree list}
+ | Ready of { }
+
+
+(* util *)
+
+fun attrsome attr f x = case x of NONE => [] | SOME x => [(attr,f x)]
+
+(* Construct output XML messages *)
+
+fun cleardisplay vs =
+ let
+ val area = #area vs
+ in
+ XML.Elem ("cleardisplay", (attrs_of_displayarea area), [])
+ end
+
+fun normalresponse vs =
+ let
+ val area = #area vs
+ val urgent = #urgent vs
+ val messagecategory = #messagecategory vs
+ val content = #content vs
+ in
+ XML.Elem ("normalresponse",
+ (attrs_of_displayarea area) @
+ (if urgent then [("urgent", "true")] else []) @
+ (attrs_of_messagecategory messagecategory),
+ content)
+ end
+
+fun errorresponse vs =
+ let
+ val area = #area vs
+ val fatality = #fatality vs
+ val location = #location vs
+ 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)),
+ content)
+ end
+
+
+fun informfile lr vs =
+ let
+ val url = #url vs
+ in
+ XML.Elem ("informfile" ^ lr, attrs_of_pgipurl url, [])
+ end
+
+val informfileloaded = informfile "loaded"
+val informfileretracted = informfile "retracted"
+
+fun proofstate vs =
+ let
+ val pgml = #pgml vs
+ in
+ XML.Elem("proofstate", [], pgml)
+ end
+
+fun metainforesponse vs =
+ let
+ val attrs = #attrs vs
+ val content = #content vs
+ in
+ XML.Elem ("metainforesponse", attrs, content)
+ end
+
+fun lexicalstructure vs =
+ let
+ val content = #content vs
+ in
+ XML.Elem ("lexicalstructure", [], content)
+ end
+
+fun proverinfo vs =
+ let
+ val name = #name vs
+ val version = #version vs
+ val instance = #instance vs
+ val descr = #descr vs
+ val url = #url vs
+ val filenameextns = #filenameextns vs
+ in
+ XML.Elem ("proverinfo",
+ [("name", name),
+ ("version", version),
+ ("instance", instance),
+ ("descr", descr),
+ ("url", Url.pack url),
+ ("filenameextns", filenameextns)],
+ [])
+ end
+
+fun idtable vs =
+ let
+ val objtype = #objtype vs
+ val objtype_attrs = [("objtype", objtype)]
+ val context = #context vs
+ val context_attrs = opt_attr "context" context
+ val ids = #ids vs
+ val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
+ in
+ XML.Elem ("idtable",
+ objtype_attrs @ context_attrs,
+ ids_content)
+ end
+
+fun setids vs =
+ let
+ val idtables = #idtables vs
+ in
+ XML.Elem ("setids",[],idtables)
+ end
+
+fun addids vs =
+ let
+ val idtables = #idtables vs
+ in
+ XML.Elem ("addids",[],idtables)
+ end
+
+fun delids vs =
+ let
+ val idtables = #idtables vs
+ in
+ XML.Elem ("delids",[],idtables)
+ end
+
+
+fun acceptedpgipelems vs =
+ let
+ val pgipelems = #pgipelems vs
+ fun async_attrs b = if b then [("async","true")] else []
+ fun attrs_attrs attrs = if attrs=[] then [] else [("attributes",space_implode "," attrs)]
+ fun singlepgipelem (e,async,attrs) =
+ XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[])
+
+ in
+ XML.Elem ("acceptedpgipelems", [],
+ map singlepgipelem pgipelems)
+ end
+
+
+fun attro x yo = case yo of NONE => [] | SOME y => [(x,y)] : XML.attributes
+
+fun hasprefs vs =
+ let
+ val prefcategory = #prefcategory vs
+ val prefs = #prefs vs
+ in
+ XML.Elem("hasprefs",attro "prefcategory" prefcategory, map haspref prefs)
+ end
+
+fun prefval vs =
+ let
+ val name = #name vs
+ val value = #value vs
+ in
+ XML.Elem("prefval", [("name",name)], [XML.Text value])
+ end
+
+fun idvalue vs =
+ let
+ val name = #name vs
+ val objtype = #objtype vs
+ val text = #text vs
+ in
+ XML.Elem("idvalue", [("name",name),("objtype",objtype)], text)
+ end
+
+
+fun informguise vs =
+ let
+ val file = #file vs
+ val theory = #theory vs
+ val theorem = #theorem vs
+ val proofpos = #proofpos vs
+
+ fun elto nm attrfn xo = case xo of NONE=>[] | SOME x=>[XML.Elem(nm,attrfn x,[])]
+
+ val guisefile = elto "guisefile" attrs_of_pgipurl file
+ val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
+ val guiseproof = elto "guiseproof"
+ (fn thm=>[("thmname",thm)]@
+ (attro "proofpos" (Option.map Int.toString proofpos))) theorem
+ in
+ XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
+ end
+
+fun parseresult vs =
+ let
+ val attrs = #attrs vs
+ val content = #content vs
+ in
+ XML.Elem("parseresult", attrs, content)
+ end
+
+fun usespgip vs =
+ let
+ val version = #version vs
+ val acceptedelems = acceptedpgipelems vs
+ in
+ XML.Elem("usespgip", [("version", version)], [acceptedelems])
+ end
+
+fun usespgml vs =
+ let
+ val version = #version vs
+ in
+ XML.Elem("usespgml", [("version", version)], [])
+ end
+
+fun pgip vs =
+ let
+ val tag = #tag vs
+ val class = #class vs
+ val seq = #seq vs
+ val id = #id vs
+ val destid = #destid vs
+ val refid = #refid vs
+ val refseq = #refseq vs
+ val content = #content vs
+ in
+ XML.Elem("pgip",
+ opt_attr "tag" tag @
+ [("id", id)] @
+ opt_attr "destid" destid @
+ [("class", class)] @
+ opt_attr "refid" refid @
+ opt_attr_map string_of_int "refseq" refseq @
+ [("seq", string_of_int seq)],
+ content)
+ end
+
+fun ready vs =
+ XML.Elem("ready",[],[])
+
+
+fun output pgipoutput = case pgipoutput of
+ Cleardisplay vs => cleardisplay vs
+ | Normalresponse vs => normalresponse vs
+ | Errorresponse vs => errorresponse vs
+ | Informfileloaded vs => informfileloaded vs
+ | Informfileretracted vs => informfileretracted vs
+ | Proofstate vs => proofstate vs
+ | Metainforesponse vs => metainforesponse vs
+ | Lexicalstructure vs => lexicalstructure vs
+ | Proverinfo vs => proverinfo vs
+ | Idtable vs => idtable vs
+ | Setids vs => setids vs
+ | Addids vs => addids vs
+ | Delids vs => delids vs
+ | Hasprefs vs => hasprefs vs
+ | Prefval vs => prefval vs
+ | Idvalue vs => idvalue vs
+ | Informguise vs => informguise vs
+ | Parseresult vs => parseresult vs
+ | Usespgip vs => usespgip vs
+ | Usespgml vs => usespgml vs
+ | Pgip vs => pgip vs
+ | Ready vs => ready vs
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgip_tests.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,91 @@
+(* Title: Pure/ProofGeneral/pgip_tests.ML
+ ID: $Id$
+ Author: David Aspinall
+
+A test suite for the PGIP abstraction code (in progress).
+Run to provide some mild insurance against breakage in Isabelle/here.
+*)
+
+(** pgip_types.ML **)
+
+local
+fun asseq_p toS a b =
+ if a=b then ()
+ else error("PGIP test: expected these two values to be equal:\n" ^
+ (toS a) ^"\n and: \n" ^ (toS b))
+
+val asseqx = asseq_p XML.string_of_tree
+val asseqs = asseq_p I
+val asseqb = asseq_p (fn b=>if b then "true" else "false")
+
+val p = XML.tree_of_string (* parse *)
+
+open PgipTypes;
+in
+
+val _ = asseqx (pgiptype_to_xml Pgipnull) (p "<pgipnull/>");
+val _ = asseqx (pgiptype_to_xml Pgipbool) (p "<pgipbool/>");
+val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (p "<pgipint/>");
+val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (p "<pgipint min='5' max='7'/>");
+val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (p "<pgipint max='7'/>");
+val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (p "<pgipint min='-5'/>");
+val _ = asseqx (pgiptype_to_xml Pgipstring) (p "<pgipstring/>");
+val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1")) (p "<pgipconst name='radio1'/>");
+val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)]))
+ (p "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
+
+val _ = asseqs (pgval_to_string (read_pgval Pgipbool "true")) "true";
+val _ = asseqs (pgval_to_string (read_pgval Pgipbool "false")) "false";
+val _ = asseqs (pgval_to_string (read_pgval (Pgipint(NONE,NONE)) "-37")) "-37";
+val _ = asseqs (pgval_to_string (read_pgval Pgipnat "45")) "45";
+val _ = asseqs (pgval_to_string (read_pgval Pgipstring "stringvalue")) "stringvalue";
+
+local
+ val choices = Pgipchoice [Pgipdtype (NONE,Pgipbool), Pgipdtype (NONE,Pgipnat),
+ Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
+in
+val _ = asseqs (pgval_to_string (read_pgval choices "45")) "45";
+val _ = asseqs (pgval_to_string (read_pgval choices "foo")) "foo";
+val _ = asseqs (pgval_to_string (read_pgval choices "true")) "true";
+val _ = asseqs (pgval_to_string (read_pgval choices "")) "";
+val _ = (asseqs (pgval_to_string (read_pgval choices "-37")) "-37";
+ error "pgip_tests: should fail") handle PGIP _ => ()
+end
+
+val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
+ default=SOME "true", pgiptype=Pgipbool})
+ (p "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
+end
+
+
+(** pgip_input.ML **)
+local
+
+val p = XML.tree_of_string (* parse *)
+
+fun e str = case p str of
+ (XML.Elem args) => args
+ | _ => error("Expected to get an XML Element")
+
+open PgipInput;
+
+fun asseqi a b =
+ if (input (e a))=b then ()
+ else error("PGIP test: expected two inputs to be equal, for input:\n" ^ a)
+
+in
+
+val _ = asseqi "<askpgip/>" (SOME (Askpgip()));
+val _ = asseqi "<askpgml/>" (SOME (Askpgml()));
+val _ = asseqi "<askconfig/>" (SOME (Askconfig()));
+val _ = asseqi "<otherelt/>" NONE;
+
+end
+
+(** pgip_output.ML **)
+local
+open PgipOutput
+in
+val _ = ()
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/pgip_types.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,371 @@
+(* Title: Pure/ProofGeneral/pgip_types.ML
+ ID: $Id$
+ Author: David Aspinall
+
+PGIP abstraction: types and conversions
+*)
+
+(* TODO: add objtypes and PGML *)
+signature PGIPTYPES =
+sig
+ (* Types and values (used for preferences and dialogs) *)
+
+ datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat
+ | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
+
+ and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *)
+
+ type pgipval (* typed value *)
+
+ (* URLs we can cope with *)
+ type pgipurl
+
+ (* Representation error in reading/writing PGIP *)
+ exception PGIP of string
+
+
+ (* Interface areas for message output *)
+ datatype displayarea = Status | Message | Display | Other of string
+
+ (* Kinds of message output (influence display behaviour) *)
+ datatype messagecategory = Normal | Information | Tracing | Internal
+
+ (* Error levels *)
+ datatype fatality = Nonfatal | Fatal | Panic | Log | Debug
+
+ (* File location *)
+ type location = { descr: string option,
+ url: pgipurl option,
+ line: int option,
+ column: int option,
+ char: int option }
+
+ (* Prover preference *)
+ type preference = { name: string,
+ descr: string option,
+ default: string option,
+ pgiptype: pgiptype }
+end
+
+signature PGIPTYPES_OPNS =
+sig
+ include PGIPTYPES
+
+ (* Values as XML strings *)
+ val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *)
+ val read_pgipnat : string -> int (* raises PGIP *)
+ val read_pgipbool : string -> bool (* raises PGIP *)
+ val read_pgipstring : string -> string (* raises PGIP *)
+ val int_to_pgstring : int -> string
+ val bool_to_pgstring : bool -> string
+ val string_to_pgstring : string -> string
+
+ (* PGIP datatypes *)
+ val pgiptype_to_xml : pgiptype -> XML.tree
+ val read_pgval : pgiptype -> string -> pgipval (* raises PGIP *)
+ val pgval_to_string : pgipval -> string
+
+ val attrs_of_displayarea : displayarea -> XML.attributes
+ val attrs_of_messagecategory : messagecategory -> XML.attributes
+ val attrs_of_fatality : fatality -> XML.attributes
+ val attrs_of_location : location -> XML.attributes
+ val location_of_attrs : XML.attributes -> location (* raises PGIP *)
+
+ val haspref : preference -> XML.tree
+
+ val pgipurl_of_url : Url.T -> pgipurl (* raises PGIP *)
+ val pgipurl_of_string : string -> pgipurl (* raises PGIP *)
+ val pgipurl_of_path : Path.T -> pgipurl
+ val attrs_of_pgipurl : pgipurl -> XML.attributes
+ val pgipurl_of_attrs : XML.attributes -> pgipurl (* raises PGIP *)
+
+ (* XML utils, only for PGIP code *)
+ val attr : string -> string -> XML.attributes
+ val opt_attr : string -> string option -> XML.attributes
+ val opt_attr_map : ('a -> string) -> string -> 'a option -> XML.attributes
+ val get_attr : string -> XML.attributes -> string (* raises PGIP *)
+ val get_attr_opt : string -> XML.attributes -> string option
+ val get_attr_dflt : string -> string -> XML.attributes -> string
+end
+
+structure PgipTypes : PGIPTYPES_OPNS =
+struct
+exception PGIP of string
+
+(** Utils **)
+
+fun get_attr_opt attr attrs = AList.lookup (op =) attrs attr
+
+fun get_attr attr attrs =
+ (case get_attr_opt attr attrs of
+ SOME value => value
+ | NONE => raise PGIP ("Missing attribute: " ^ attr))
+
+fun get_attr_dflt attr dflt attrs = the_default dflt (get_attr_opt attr attrs)
+
+fun attr x y = [(x,y)] : XML.attributes
+
+fun opt_attr_map f attr_name opt_val =
+ case opt_val of NONE => [] | SOME v => [(attr_name,f v)]
+ (* or, if you've got function-itis:
+ the_default [] (Option.map (single o (pair attr_name) o f) opt_val)
+ *)
+
+val opt_attr = opt_attr_map I
+
+(** Types and values **)
+
+(* readers and writers for values represented in XML strings *)
+
+fun read_pgipbool s =
+ (case s of
+ "false" => false
+ | "true" => true
+ | _ => raise PGIP ("Invalid boolean value: "^s))
+
+local
+ fun int_in_range (NONE,NONE) _ = true
+ | int_in_range (SOME min,NONE) i = min<= i
+ | int_in_range (NONE,SOME max) i = i<=max
+ | int_in_range (SOME min,SOME max) i = min<= i andalso i<=max
+in
+fun read_pgipint range s =
+ (case Syntax.read_int s of
+ SOME i => if int_in_range range i then i
+ else raise PGIP ("Out of range integer value: "^s)
+ | NONE => raise PGIP ("Invalid integer value: "^s))
+end;
+
+fun read_pgipnat s =
+ (case Syntax.read_nat s of
+ SOME i => i
+ | NONE => raise PGIP ("Invalid natural number: "^s))
+
+(* NB: we can maybe do without xml decode/encode here. *)
+fun read_pgipstring s = (* non-empty strings, XML escapes decoded *)
+ (case XML.parse_string s of
+ SOME s => s
+ | NONE => raise PGIP ("Expected a non-empty string: "^s))
+ handle _ => raise PGIP ("Invalid XML string syntax: "^s)
+
+fun int_to_pgstring i =
+ if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i
+
+fun string_to_pgstring s = XML.text s
+
+fun bool_to_pgstring b = if b then "true" else "false"
+
+
+(* PGIP datatypes.
+
+ This is a reflection of the type structure of PGIP configuration,
+ which is meant for setting up user dialogs and preference settings.
+ These are configured declaratively in XML, using a syntax for types
+ and values which is like a (vastly cut down) form of XML Schema
+ Datatypes.
+
+ The prover needs to interpret the strings representing the typed
+ values, at least for the types it expects from the dialogs it
+ configures. Here we go further and construct a type-safe
+ encapsulation of these values, which would be useful for more
+ advanced cases (e.g. generating and processing forms).
+*)
+
+
+datatype pgiptype =
+ Pgipnull (* unit type: unique element is empty string *)
+ | Pgipbool (* booleans: "true" or "false" *)
+ | Pgipint of int option * int option (* ranged integers, should be XSD canonical *)
+ | Pgipnat (* naturals: non-negative integers (convenience) *)
+ | Pgipstring (* non-empty strings *)
+ | Pgipconst of string (* singleton type *)
+ | Pgipchoice of pgipdtype list (* union type *)
+
+(* Compared with the PGIP schema, we push descriptions of types inside choices. *)
+
+and pgipdtype = Pgipdtype of string option * pgiptype
+
+datatype pgipuval = Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int
+ | Pgvalstring of string | Pgvalconst of string
+
+type pgipval = pgiptype * pgipuval (* type-safe values *)
+
+fun pgipdtype_to_xml (desco,ty) =
+ let
+ val desc_attr = opt_attr "descr" desco
+
+ val elt = case ty of
+ Pgipnull => "pgipnull"
+ | Pgipbool => "pgipbool"
+ | Pgipint _ => "pgipint"
+ | Pgipnat => "pgipint"
+ | Pgipstring => "pgipstring"
+ | Pgipconst _ => "pgipconst"
+ | Pgipchoice _ => "pgipchoice"
+
+ fun range_attr r v = attr r (int_to_pgstring v)
+
+ val attrs = case ty of
+ Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max)
+ | Pgipint (SOME min,NONE) => (range_attr "min" min)
+ | Pgipint (NONE,SOME max) => (range_attr "max" max)
+ | Pgipnat => (range_attr "min" 0)
+ | Pgipconst nm => attr "name" nm
+ | _ => []
+
+ fun destpgipdtype (Pgipdtype x) = x
+
+ val typargs = case ty of
+ Pgipchoice ds => map destpgipdtype ds
+ | _ => []
+ in
+ XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
+ end
+
+val pgiptype_to_xml = pgipdtype_to_xml o (pair NONE)
+
+fun read_pguval Pgipnull s =
+ if s="" then Pgvalnull
+ else raise PGIP ("Expecting empty string for null type, not: "^s)
+ | read_pguval Pgipbool s = Pgvalbool (read_pgipbool s)
+ | read_pguval (Pgipint range) s = Pgvalint (read_pgipint range s)
+ | read_pguval Pgipnat s = Pgvalnat (read_pgipnat s)
+ | read_pguval (Pgipconst c) s =
+ if c=s then Pgvalconst c
+ else raise PGIP ("Given string: "^s^" doesn't match expected string: "^c)
+ | read_pguval Pgipstring s =
+ if s<>"" then Pgvalstring s
+ else raise PGIP ("Expecting non-empty string, empty string illegal.")
+ | read_pguval (Pgipchoice tydescs) s =
+ let
+ (* Union type: match first in list *)
+ fun getty (Pgipdtype(_,ty)) = ty
+ val uval = get_first
+ (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
+ (map getty tydescs)
+ in
+ case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^s^
+ " against any allowed types.")
+ end
+
+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
+
+
+(** URLs: only local files **)
+
+type pgipurl = Path.T
+
+datatype displayarea = Status | Message | Display | Other of string
+
+datatype messagecategory = Normal | Information | Tracing | Internal
+
+datatype fatality = Nonfatal | Fatal | Panic | Log | Debug
+
+type location = { descr: string option,
+ url: pgipurl option,
+ line: int option,
+ column: int option,
+ char: int option }
+
+
+
+(** Url operations **)
+
+fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
+ case Url.unpack url of
+ (Url.File path) => path
+ | _ => raise PGIP ("Cannot access non-local URL " ^ url)
+
+fun pgipurl_of_path p = p
+
+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")
+
+fun pgipurl_of_url (Url.File p) = p
+ | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.pack url))
+
+
+(** Messages and errors **)
+
+local
+ fun string_of_area Status = "status"
+ | string_of_area Message = "message"
+ | string_of_area Display = "display"
+ | string_of_area (Other s) = s
+
+ fun string_of_msgcat Internal = "internal"
+ | string_of_msgcat Information = "information"
+ | string_of_msgcat Tracing = "tracing"
+ | string_of_msgcat Normal = "normal" (* omitted in PGIP *)
+
+ fun string_of_fatality Nonfatal = "nonfatal"
+ | string_of_fatality Fatal = "fatal"
+ | string_of_fatality Panic = "panic"
+ | string_of_fatality Log = "log"
+ | string_of_fatality Debug = "debug"
+in
+ fun attrs_of_displayarea area = [("area", string_of_area area)]
+
+ fun attrs_of_messagecategory msgcat =
+ case msgcat of
+ Normal => []
+ | _ => [("messagecategory", string_of_msgcat msgcat)]
+
+ fun attrs_of_fatality fatality = [("fatality", string_of_fatality fatality)]
+
+ 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 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
+ in
+ descr @ url @ line @ column @ char
+ end
+
+ fun pgipint_of_string err s =
+ case Syntax.read_int s of
+ SOME i => i
+ | NONE => raise PGIP ("Type error in " ^ err ^ ": expected integer.")
+
+ fun location_of_attrs attrs =
+ let
+ val descr = get_attr_opt "descr" attrs
+ val url = Option.map pgipurl_of_string (get_attr_opt "url" attrs)
+ val line = Option.map (pgipint_of_string "location element line attribute")
+ (get_attr_opt "line" attrs)
+ val column = Option.map (pgipint_of_string "location element column attribute")
+ (get_attr_opt "column" attrs)
+ val char = Option.map (pgipint_of_string "location element char attribute")
+ (get_attr_opt "char" attrs)
+ in
+ {descr=descr, url=url, line=line, column=column, char=char}
+ end
+end
+
+(** Preferences **)
+
+type preference = { name: string,
+ descr: string option,
+ default: string option,
+ pgiptype: pgiptype }
+
+fun haspref ({ name, descr, default, pgiptype}:preference) =
+ XML.Elem ("haspref",
+ attr "name" name @
+ opt_attr "descr" descr @
+ opt_attr "default" default,
+ [pgiptype_to_xml pgiptype])
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/preferences.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,153 @@
+(* Title: Pure/ProofGeneral/preferences.ML
+ ID: $Id$
+ Author: David Aspinall and Markus Wenzel
+
+User preferences for Isabelle which are maintained by the interface.
+*)
+
+signature PREFERENCES =
+sig
+ type pgiptype = PgipTypes.pgiptype
+
+ type isa_preference = { name: string,
+ descr: string,
+ default: string,
+ pgiptype: pgiptype,
+ get: unit -> string,
+ set: string -> unit }
+
+ val preferences : (string * isa_preference list) list
+end
+
+structure Preferences : PREFERENCES =
+struct
+
+val thm_depsN = "thm_deps"; (* also in proof_general_pgip.ML: move to pgip_isabelle? *)
+
+type pgiptype = PgipTypes.pgiptype
+
+type isa_preference = { name: string,
+ descr: string,
+ default: string,
+ pgiptype: pgiptype,
+ get: unit -> string,
+ set: string -> unit }
+
+
+fun mkpref get set typ nm descr =
+ { name=nm, descr=descr, pgiptype=typ, get=get, set=set, default=get() } : isa_preference
+
+fun mkpref_from_ref read write typ r nm descr =
+ mkpref (fn()=> read (!r)) (fn v=> r:= (write v)) typ nm descr
+
+val int_pref =
+ mkpref_from_ref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE,NONE))
+ (PgipTypes.Pgipint (NONE, NONE))
+val nat_pref =
+ mkpref_from_ref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat
+
+val bool_pref =
+ mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool
+
+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)
+ in
+ mkpref get set PgipTypes.Pgipbool "full-proofs"
+ "Record full proof objects internally"
+ end
+
+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
+ change print_mode (insert (op =) thm_depsN)
+ else
+ change print_mode (remove (op =) thm_depsN)
+ in
+ mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
+ "Track theorem dependencies within Proof General"
+ end
+
+val print_depth_pref =
+ let
+ val pg_print_depth_val = ref 10
+ fun get () = PgipTypes.int_to_pgstring (! pg_print_depth_val)
+ fun setn n = (print_depth n; pg_print_depth_val := n)
+ val set = setn o PgipTypes.read_pgipnat
+ in
+ mkpref get set PgipTypes.Pgipbool "print-depth" "Setting for the ML print depth"
+ end
+
+
+val display_preferences =
+ [bool_pref show_types
+ "show-types"
+ "Include types in display of Isabelle terms",
+ bool_pref show_sorts
+ "show-sorts"
+ "Include sorts in display of Isabelle terms",
+ bool_pref show_consts
+ "show-consts"
+ "Show types of consts in Isabelle goal display",
+ bool_pref long_names
+ "long-names"
+ "Show fully qualified names in Isabelle terms",
+ bool_pref show_brackets
+ "show-brackets"
+ "Show full bracketing in Isabelle terms",
+ bool_pref Proof.show_main_goal
+ "show-main-goal"
+ "Show main goal in proof state display",
+ bool_pref Syntax.eta_contract
+ "eta-contract"
+ "Print terms eta-contracted"]
+
+val advanced_display_preferences =
+ [nat_pref goals_limit
+ "goals-limit"
+ "Setting for maximum number of goals printed",
+ int_pref ProofContext.prems_limit
+ "prems-limit"
+ "Setting for maximum number of premises printed",
+ print_depth_pref,
+ bool_pref show_question_marks
+ "show-question-marks"
+ "Show leading question mark of variable name"]
+
+val tracing_preferences =
+ [bool_pref trace_simp
+ "trace-simplifier"
+ "Trace simplification rules.",
+ nat_pref trace_simp_depth_limit
+ "trace-simplifier-depth"
+ "Trace simplifier depth limit.",
+ bool_pref trace_rules
+ "trace-rules"
+ "Trace application of the standard rules",
+ bool_pref Pattern.trace_unify_fail
+ "trace-unification"
+ "Output error diagnostics during unification",
+ bool_pref Output.timing
+ "global-timing"
+ "Whether to enable timing in Isabelle.",
+ bool_pref Output.show_debug_msgs
+ "debug-messages"
+ "Whether to show debugging messages."]
+
+val proof_preferences =
+ [bool_pref quick_and_dirty
+ "quick-and-dirty"
+ "Take a few short cuts",
+ bool_pref Toplevel.skip_proofs
+ "skip-proofs"
+ "Ignore proof scripts (interactive-only)"]
+
+val preferences =
+ [("Display", display_preferences),
+ ("Advanced Display", advanced_display_preferences),
+ ("Tracing", tracing_preferences),
+ ("Proof", proof_preferences)]
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Dec 04 20:40:11 2006 +0100
@@ -0,0 +1,1002 @@
+(* Title: Pure/ProofGeneral/proof_general_pgip.ML
+ ID: $Id$
+ Author: David Aspinall and Markus Wenzel
+
+Isabelle configuration for Proof General using PGIP protocol.
+See http://proofgeneral.inf.ed.ac.uk/kit
+*)
+
+
+signature PROOF_GENERAL_PGIP =
+sig
+ val init_pgip: bool -> unit
+end
+
+structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
+struct
+
+structure P = OuterParse;
+
+open Pgip;
+
+(* 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*)
+
+
+(* 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 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;
+
+(* XML immediately rendered pretty printer. Take care not to double escape *)
+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.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 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
+
+val class_tag = "class"
+val tfree_tag = "tfree"
+val tvar_tag = "tvar"
+val free_tag = "free"
+val bound_tag = "bound"
+val var_tag = "var"
+val skolem_tag = "skolem"
+
+fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
+
+fun tagit kind x =
+ (xml_atom kind x, 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 and issuing PGIP packets **)
+
+val pgip_refid = ref NONE: string option ref;
+val pgip_refseq = ref NONE: int 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 =
+ 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 () =
+ pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
+ getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
+
+fun matching_pgip_id id = (id = !pgip_id)
+
+val output_xml = writeln_default o XML.string_of_tree; (* FIXME: use string buffer *)
+
+fun issue_pgip_rawtext str =
+ output_xml (PgipOutput.output (assemble_pgips [XML.Text str])) (* FIXME: don't escape!! *)
+
+fun issue_pgips pgipops =
+ output_xml (PgipOutput.output (assemble_pgips (map PgipOutput.output pgipops)));
+
+fun issue_pgip pgipop =
+ output_xml (PgipOutput.output (assemble_pgips [PgipOutput.output pgipop]));
+
+end;
+
+
+(** messages and notification **)
+
+local
+ val delay_msgs = ref false (*true: accumulate messages*)
+ val delayed_msgs = ref []
+
+ fun queue_or_issue pgip =
+ if (! delay_msgs) then
+ delayed_msgs := pgip :: ! delayed_msgs
+ else issue_pgip pgip
+in
+ fun normalmsg area cat urgent prfx s =
+ let
+ val content =
+ (* NB: prefixing is obsolete, but let's keep it for a while for familiarity *)
+ XML.Elem("pgmltext",[],[XML.Rawtext (prefix_lines prfx s)])
+ val pgip = Normalresponse {area=area,messagecategory=cat,
+ urgent=urgent,content=[content] }
+ in
+ queue_or_issue pgip
+ end
+
+ fun errormsg fatality prfx s =
+ let
+ (* FIXME: need a way of passing in locations *)
+ val content =
+ XML.Elem("pgmltext",[],[XML.Rawtext (prefix_lines prfx s)])
+ val pgip = Errorresponse {area=NONE,fatality=fatality,
+ content=[content], 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)
+end;
+
+(* 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
+ enough to use Rawtext always above. *)
+
+fun setup_messages () =
+ (writeln_fn := (fn s => normalmsg Message Normal false "" s);
+ priority_fn := (fn s => normalmsg Message Normal true "" s);
+ tracing_fn := (fn s => normalmsg Message Tracing false "" s);
+ info_fn := (fn s => normalmsg Message Information false "+++ " s);
+ debug_fn := (fn s => normalmsg Message Internal false "+++ " s);
+ warning_fn := (fn s => errormsg Nonfatal "### " s);
+ error_fn := (fn s => errormsg Fatal "*** " s);
+ panic_fn := (fn s => errormsg Panic "!!! " s))
+
+(* immediate messages *)
+
+fun tell_clear_goals () = issue_pgip (Cleardisplay {area=Display})
+fun tell_clear_response () = issue_pgip (Cleardisplay {area=Message})
+fun tell_file_loaded path = issue_pgip (Informfileloaded {url=PgipTypes.pgipurl_of_path path})
+fun tell_file_retracted path = issue_pgip (Informfileretracted {url=PgipTypes.pgipurl_of_path path})
+
+
+
+(** theory / proof state output **)
+
+local
+
+fun statedisplay prts =
+ let
+ val display = Pretty.output (Pretty.chunks prts)
+ val statedisplay = XML.Elem("statedisplay",[], [XML.Rawtext display])
+ in
+ issue_pgip (Proofstate {pgml=[XML.Elem("pgml",[],[statedisplay])]})
+ end
+
+fun print_current_goals n m st =
+ statedisplay (Display.pretty_current_goals n m st)
+
+fun print_state b st =
+ statedisplay (Toplevel.pretty_state b st)
+
+in
+
+fun setup_state () =
+ (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))); *)
+
+end;
+
+
+(* 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.pack o #1 o Path.split_ext o Path.base o Path.unpack;
+
+(* 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.unpack 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.unpack file))))
+ else raise Toplevel.UNDEF
+ end;
+
+fun vacuous_inform_file_processed file state =
+ (warning ("No theory " ^ quote (thy_name file));
+ tell_file_retracted (Path.base (Path.unpack file)));
+
+
+(* restart top-level loop (keeps most state information) *)
+
+val welcome = priority o Session.welcome;
+
+fun restart () =
+ (sync_thy_loader ();
+ tell_clear_goals ();
+ tell_clear_response ();
+ welcome ();
+ raise Toplevel.RESTART)
+
+
+(* theorem dependency output *)
+local
+
+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])
+ in
+ issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")],
+ content=[valuethms,valuedeps]})
+ end
+
+(* 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 Thm.name_of_thm 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;
+
+(** 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.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()) }
+ 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 *)
+
+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 config_file() = orenv "ISABELLE_PGIPCONFIG" staticconfig
+ fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" isabellewww
+in
+fun send_pgip_config () =
+ let
+ val path = Path.unpack (config_file())
+ val exists = File.exists path
+
+ val wwwpage =
+ (Url.unpack (isabelle_www()))
+ handle _ =>
+ (Output.panic
+ ("Error in URL in environment variable ISABELLE_HOMEPAGE.");
+ Url.unpack isabellewww)
+
+ val proverinfo =
+ Proverinfo { name = "Isabelle",
+ 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()))
+ else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
+ end;
+end
+
+
+(* PGIP identifier tables (prover objects). [incomplete] *)
+
+local
+ (* TODO: objtypes should be in pgip_types.ML *)
+ val objtype_thy = "theory"
+ val objtype_thm = "theorem"
+ val objtype_term = "term"
+ val objtype_type = "type"
+
+ fun xml_idtable ty ctx ids =
+ PgipOutput.output (Idtable {objtype=ty,context=ctx,ids=ids})
+in
+
+fun setids t = issue_pgip (Setids {idtables = [t]})
+fun addids t = issue_pgip (Addids {idtables = [t]})
+fun delids t = issue_pgip (Delids {idtables = [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
+
+
+(* Sending commands to Isar *)
+
+fun isarcmd s =
+ s |> OuterSyntax.scan |> OuterSyntax.read
+ |> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;
+
+(* how TODO: apply a command given a transition function, e.g. IsarCmd.undo *)
+
+(* load an arbitrary file (must be .thy or .ML) *)
+
+fun use_thy_or_ml_file file =
+ let
+ val (path,extn) = Path.split_ext (Path.unpack file)
+ in
+ case extn of
+ "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
+ | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
+ | "ML" => isarcmd ("use " ^ quote file)
+ | other => error ("Don't know how to read a file with extension " ^ other)
+ end
+
+
+(**** PGIP actions ****)
+
+
+(* Responses to each of the PGIP input commands.
+ These are programmed uniformly for extensibility. *)
+
+fun askpgip vs =
+ issue_pgip
+ (Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
+ pgipelems = PgipIsabelle.accepted_inputs })
+
+fun askpgml vs =
+ issue_pgip
+ (Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
+
+fun askprefs vs =
+ 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}))
+ Preferences.preferences
+ end
+
+fun 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
+in
+fun setpref vs =
+ let
+ val name = #name vs
+ val value = #value vs
+ val set = #set (lookuppref name)
+ in
+ set value
+ end
+
+fun getpref vs =
+ let
+ val name = #name vs
+ val get = #get (lookuppref name)
+ in
+ issue_pgip (Prefval {name=name, value=get ()})
+ end
+end
+
+fun proverinit vs = restart ()
+
+fun proverexit vs = isarcmd "quit"
+
+fun startquiet vs = isarcmd "disable_pr"
+
+fun stopquiet vs = isarcmd "enable_pr"
+
+fun pgmlsymbolson vs =
+ change print_mode (fn mode =>
+ remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
+
+fun pgmlsymbolsoff vs =
+ change print_mode (remove (op =) Symbol.xsymbolsN)
+
+fun dostep vs =
+ let
+ val text = #text vs
+ in
+ isarcmd text
+ end
+
+fun undostep vs =
+ 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 askids vs =
+ let
+ val thyname = #thyname vs
+ val objtype = #objtype vs
+ in
+ (* TODO: add askids for "file" here, which returns single theory with same name *)
+ case (thyname,objtype) of
+ (* only theories known in top context *)
+ (NONE, NONE) => send_thy_idtable NONE (ThyInfo.names())
+ | (NONE, SOME "theory") => send_thy_idtable NONE (ThyInfo.names())
+ | (SOME thy, SOME "theory") => send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
+ | (SOME thy, SOME "theorem") => send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
+ | (SOME thy, NONE) => (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
+ send_thm_idtable (SOME thy) (ThyInfo.get_theory thy))
+ | (_, SOME ot) => error ("No objects of type "^(quote ot)^" are available here.")
+ end
+
+local
+ (* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
+ fun with_displaywrap pgipfn dispfn =
+ let
+ val lines = ref ([]: string list);
+ fun wlgrablines s = lines := s :: ! lines;
+ in
+ setmp writeln_fn wlgrablines dispfn ();
+ issue_pgip (pgipfn (!lines))
+ end;
+in
+fun showid vs =
+ let
+ val thyname = #thyname vs
+ val objtype = #objtype vs
+ val name = #objtype 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 pthm thy name = print_thm (get_thm thy (Name name))
+ in
+ case (thyname, objtype) of
+ (_,"theory") =>
+ with_displaywrap (idvalue "theory" name)
+ (fn ()=>(print_theory (ThyInfo.get_theory name)))
+ | (SOME thy, "theorem") =>
+ with_displaywrap (idvalue "theorem" name)
+ (fn ()=>(pthm (ThyInfo.get_theory thy) name))
+ | (NONE, "theorem") =>
+ with_displaywrap (idvalue "theorem" name)
+ (fn ()=>pthm (topthy()) name)
+ | (_, ot) => error ("Cannot show objects of type "^ot)
+ end
+
+(* 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.
+*)
+
+val currently_open_file = ref (NONE : pgipurl option)
+
+fun askguise vs =
+ (* The "guise" is the PGIP abstraction of the prover's state.
+ The <informguise> message is merely used for consistency checking. *)
+ let
+ val openfile = !currently_open_file
+
+ 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
+
+ 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 })
+ end
+
+fun parsescript vs =
+ let
+ val text = #text vs
+ val systemdata = #systemdata vs
+ val location = #location vs (* TODO: extract position *)
+
+ val _ = start_delay_msgs () (* gather parsing messages *)
+ val xmls = PgipParser.xmls_of_str text
+ val errs = end_delayed_msgs ()
+
+ val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
+ val locattrs = PgipTypes.attrs_of_location location
+ in
+ issue_pgip (Parseresult { attrs= sysattrs@locattrs,
+ content = (map PgipOutput.output errs)@xmls })
+ end
+
+fun showproofstate vs = isarcmd "pr"
+
+fun showctxt vs = isarcmd "print_theory" (* more useful than print_context *)
+
+fun searchtheorems vs =
+ let
+ val arg = #arg vs
+ in
+ isarcmd ("thms_containing " ^ arg)
+ end
+
+fun setlinewidth vs =
+ let
+ val width = #width vs
+ in
+ isarcmd ("pretty_setmargin " ^ (Int.toString width)) (* FIXME: conversion back/forth! *)
+ end
+
+fun viewdoc vs =
+ let
+ val arg = #arg vs
+ in
+ isarcmd ("print_" ^ arg) (* FIXME: isatool doc?. Return URLs, maybe? *)
+ end
+
+fun doitem vs =
+ let
+ val text = #text vs
+ in
+ isarcmd text
+ end
+
+fun undoitem vs =
+ isarcmd "ProofGeneral.undo"
+
+fun redoitem vs =
+ isarcmd "ProofGeneral.redo"
+
+fun aborttheory vs =
+ isarcmd "init_toplevel"
+
+fun retracttheory vs =
+ let
+ val thyname = #thyname vs
+ in
+ isarcmd ("kill_thy " ^ quote thyname)
+ end
+
+fun loadfile vs =
+ let
+ val url = #url vs
+ in
+ case !currently_open_file of
+ SOME f => raise PGIP ("<loadfile> when a file is open!")
+ | NONE => use_thy_or_ml_file (File.platform_path url)
+ end
+
+fun openfile vs =
+ let
+ val url = #url vs
+ in
+ case !currently_open_file of
+ SOME f => raise PGIP ("<openfile> when a file is already open! ")
+ | NONE => (openfile_retract (File.platform_path url);
+ currently_open_file := SOME url) (*(File.platform_path url))*)
+ end
+
+fun closefile vs =
+ case !currently_open_file of
+ SOME f => (proper_inform_file_processed (File.platform_path f)
+ (Isar.state());
+ currently_open_file := NONE)
+ | NONE => raise PGIP ("<closefile> when no file is open!")
+
+fun abortfile vs =
+ case !currently_open_file of
+ SOME f => (isarcmd "init_toplevel";
+ currently_open_file := NONE)
+ | NONE => raise PGIP ("<abortfile> when no file is open!")
+
+fun retractfile vs =
+ let
+ val url = #url vs
+ in
+ case !currently_open_file of
+ SOME f => raise PGIP ("<retractfile> when a file is open!")
+ | NONE => inform_file_retracted (File.platform_path url)
+ end
+
+(* 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 assume that the prover has a load path.
+*)
+
+local
+ val current_working_dir = ref (NONE : string option)
+in
+fun changecwd vs =
+ let
+ val url = #url vs
+ val newdir = File.platform_path url
+ in
+ (case (!current_working_dir) of
+ NONE => ()
+ | SOME dir => ThyLoad.del_path dir;
+ ThyLoad.add_path newdir;
+ current_working_dir := SOME newdir)
+ end
+end
+
+
+fun systemcmd vs =
+ let
+ val arg = #arg vs
+ in
+ isarcmd arg
+ end
+
+exception PGIP_QUIT;
+fun quitpgip vs = raise PGIP_QUIT
+
+fun process_input inp = case inp of
+ Pgip.Askpgip vs => askpgip vs
+ | Pgip.Askpgml vs => askpgml vs
+ | Pgip.Askprefs vs => askprefs vs
+ | Pgip.Askconfig vs => askconfig vs
+ | Pgip.Getpref vs => getpref vs
+ | Pgip.Setpref vs => setpref vs
+ | Pgip.Proverinit vs => proverinit vs
+ | Pgip.Proverexit vs => proverexit vs
+ | Pgip.Startquiet vs => startquiet vs
+ | Pgip.Stopquiet vs => stopquiet vs
+ | Pgip.Pgmlsymbolson vs => pgmlsymbolson vs
+ | Pgip.Pgmlsymbolsoff vs => pgmlsymbolsoff vs
+ | Pgip.Dostep vs => dostep vs
+ | Pgip.Undostep vs => undostep vs
+ | Pgip.Redostep vs => redostep vs
+ | Pgip.Forget vs => (error "<forget> not implemented")
+ | Pgip.Restoregoal vs => (error "<restoregoal> not implemented")
+ | Pgip.Abortgoal vs => abortgoal vs
+ | Pgip.Askids vs => askids vs
+ | Pgip.Showid vs => showid vs
+ | Pgip.Askguise vs => askguise vs
+ | Pgip.Parsescript vs => parsescript vs
+ | Pgip.Showproofstate vs => showproofstate vs
+ | Pgip.Showctxt vs => showctxt vs
+ | Pgip.Searchtheorems vs => searchtheorems vs
+ | Pgip.Setlinewidth vs => setlinewidth vs
+ | Pgip.Viewdoc vs => viewdoc vs
+ | Pgip.Doitem vs => doitem vs
+ | Pgip.Undoitem vs => undoitem vs
+ | Pgip.Redoitem vs => redoitem vs
+ | Pgip.Aborttheory vs => aborttheory vs
+ | Pgip.Retracttheory vs => retracttheory vs
+ | Pgip.Loadfile vs => loadfile vs
+ | Pgip.Openfile vs => openfile vs
+ | Pgip.Closefile vs => closefile vs
+ | Pgip.Abortfile vs => abortfile vs
+ | Pgip.Retractfile vs => retractfile vs
+ | Pgip.Changecwd vs => changecwd vs
+ | Pgip.Systemcmd vs => systemcmd vs
+ | Pgip.Quitpgip vs => quitpgip vs
+
+
+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.Text 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)
+ else ()
+
+fun process_pgip_tree xml =
+ (pgip_refid := NONE;
+ pgip_refseq := NONE;
+ (case xml of
+ XML.Elem ("pgip", attrs, pgips) =>
+ (let
+ val class = PgipTypes.get_attr "class" attrs
+ val dest = PgipTypes.get_attr_opt "destid" attrs
+ val _ = (pgip_refid := PgipTypes.get_attr_opt "id" attrs)
+ val _ = (pgip_refseq := Option.join
+ (Option.map Int.fromString
+ (PgipTypes.get_attr_opt "seq" attrs)))
+ (* Respond to prover broadcasts, or messages for us. Ignore rest *)
+ val processit =
+ case dest of
+ NONE => class = "pa"
+ | SOME id => matching_pgip_id id
+ in
+ if processit then
+ (List.app process_pgip_element pgips; true)
+ else 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))
+
+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_pgip (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) (* error in XML parse or Ready issue *)
+
+and handler (e,srco) =
+ case (e,srco) of
+ (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)
+ | (_,NONE) => ()
+in
+ (* TODO: add socket interface *)
+
+ 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 *)
+(* da: TODO: perhaps we can drop this superfluous syntax now??
+ Seems cleaner to support the operations directly above in the PGIP actions.
+ *)
+
+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));
+
+(* da: what were these context commands ones for? *)
+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)));
+
+(* ProofGeneral.kill_proof still used above *)
+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));
+
+(* FIXME: Not quite same as commands used above *)
+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))));
+
+(* This one can actually be used for Daniel's interface scripting idea: generically!! *)
+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, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
+ inform_file_processedP, inform_file_retractedP, process_pgipP];
+
+end;
+
+
+(* init *)
+
+val initialized = ref false;
+
+(* ML top level only for testing, entered on <quitpgip> *)
+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_pgml_output ();
+ setup_messages ();
+ setup_state ();
+ setup_thy_loader ();
+ setup_present_hook ();
+ init_pgip_session_id ();
+ welcome ();
+ set initialized; ()));
+ sync_thy_loader ();
+ change print_mode (cons proof_generalN o remove (op =) proof_generalN);
+ change print_mode (append [pgmlN, pgmlatomsN] o subtract (op =) [pgmlN, pgmlatomsN]);
+ set_prompts ());
+
+fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode."
+ | init_pgip true = (init_setup (); pgip_toplevel tty_src);
+
+fun write_keywords s = () (* NB: do nothing *)
+
+end;
+