--- a/src/Pure/ProofGeneral/parsing.ML Fri Dec 22 21:00:55 2006 +0100
+++ b/src/Pure/ProofGeneral/parsing.ML Wed Dec 27 16:18:07 2006 +0100
@@ -245,7 +245,7 @@
let
val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
in
- if (prewhs <> []) then
+ if not (null prewhs) then
D.Whitespace {text=implode (map OuterLex.unparse prewhs)}
:: (markup_comment_whs rest)
else
@@ -299,9 +299,10 @@
(* 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 (t::ts, w::ws, vs) =
+ if OuterLex.eq_token (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 pgip_parser str =
--- a/src/Pure/ProofGeneral/pgip_output.ML Fri Dec 22 21:00:55 2006 +0100
+++ b/src/Pure/ProofGeneral/pgip_output.ML Wed Dec 27 16:18:07 2006 +0100
@@ -105,15 +105,15 @@
(* Construct output XML messages *)
-
-fun cleardisplay vs =
+
+fun cleardisplay (Cleardisplay vs) =
let
val area = #area vs
in
XML.Elem ("cleardisplay", (attrs_of_displayarea area), [])
end
-fun normalresponse vs =
+fun normalresponse (Normalresponse vs) =
let
val area = #area vs
val urgent = #urgent vs
@@ -126,8 +126,8 @@
(attrs_of_messagecategory messagecategory),
content)
end
-
-fun errorresponse vs =
+
+fun errorresponse (Errorresponse vs) =
let
val area = #area vs
val fatality = #fatality vs
@@ -140,26 +140,29 @@
(the_default [] (Option.map attrs_of_location location)),
content)
end
-
-fun informfile lr vs =
+fun informfileloaded (Informfileloaded vs) =
let
val url = #url vs
in
- XML.Elem ("informfile" ^ lr, attrs_of_pgipurl url, [])
+ XML.Elem ("informfileloaded", attrs_of_pgipurl url, [])
end
-val informfileloaded = informfile "loaded"
-val informfileretracted = informfile "retracted"
+fun informfileretracted (Informfileretracted vs) =
+ let
+ val url = #url vs
+ in
+ XML.Elem ("informfileretracted", attrs_of_pgipurl url, [])
+ end
-fun proofstate vs =
+fun proofstate (Proofstate vs) =
let
val pgml = #pgml vs
in
XML.Elem("proofstate", [], pgml)
end
-fun metainforesponse vs =
+fun metainforesponse (Metainforesponse vs) =
let
val attrs = #attrs vs
val content = #content vs
@@ -167,14 +170,14 @@
XML.Elem ("metainforesponse", attrs, content)
end
-fun lexicalstructure vs =
+fun lexicalstructure (Lexicalstructure vs) =
let
val content = #content vs
in
XML.Elem ("lexicalstructure", [], content)
end
-fun proverinfo vs =
+fun proverinfo (Proverinfo vs) =
let
val name = #name vs
val version = #version vs
@@ -193,43 +196,28 @@
[])
end
-fun setids vs =
+fun setids (Setids vs) =
let
val idtables = #idtables vs
in
XML.Elem ("setids",[],map idtable_to_xml idtables)
end
-fun addids vs =
+fun addids (Addids vs) =
let
val idtables = #idtables vs
in
XML.Elem ("addids",[],map idtable_to_xml idtables)
end
-fun delids vs =
+fun delids (Delids vs) =
let
val idtables = #idtables vs
in
XML.Elem ("delids",[],map idtable_to_xml idtables)
end
-
-fun acceptedpgipelems vs =
- let
- val pgipelems = #pgipelems vs
- fun async_attrs b = if b then attr "async" "true" else []
- fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
- fun singlepgipelem (e,async,attrs) =
- XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[XML.Text e])
-
- in
- XML.Elem ("acceptedpgipelems", [],
- map singlepgipelem pgipelems)
- end
-
-
-fun hasprefs vs =
+fun hasprefs (Hasprefs vs) =
let
val prefcategory = #prefcategory vs
val prefs = #prefs vs
@@ -237,7 +225,7 @@
XML.Elem("hasprefs",opt_attr "prefcategory" prefcategory, map haspref prefs)
end
-fun prefval vs =
+fun prefval (Prefval vs) =
let
val name = #name vs
val value = #value vs
@@ -245,17 +233,16 @@
XML.Elem("prefval", attr "name" name, [XML.Text value])
end
-fun idvalue vs =
+fun idvalue (Idvalue vs) =
let
val name = #name vs
val objtype_attrs = attrs_of_objtype (#objtype vs)
val text = #text vs
in
XML.Elem("idvalue", attr "name" name @ objtype_attrs, text)
- end
+ end
-
-fun informguise vs =
+fun informguise (Informguise vs) =
let
val file = #file vs
val theory = #theory vs
@@ -273,7 +260,7 @@
XML.Elem("informguise", [], guisefile @ guisetheory @ guiseproof)
end
-fun parseresult vs =
+fun parseresult (Parseresult vs) =
let
val attrs = #attrs vs
val doc = #doc vs
@@ -283,22 +270,35 @@
XML.Elem("parseresult", attrs, errs@xmldoc)
end
-fun usespgip vs =
+fun acceptedpgipelems (Usespgip vs) =
+ let
+ val pgipelems = #pgipelems vs
+ fun async_attrs b = if b then attr "async" "true" else []
+ fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
+ fun singlepgipelem (e,async,attrs) =
+ XML.Elem("pgipelem", ((async_attrs async) @ (attrs_attrs attrs)),[XML.Text e])
+
+ in
+ XML.Elem ("acceptedpgipelems", [],
+ map singlepgipelem pgipelems)
+ end
+
+fun usespgip (Usespgip vs) =
let
val version = #version vs
- val acceptedelems = acceptedpgipelems vs
+ val acceptedelems = acceptedpgipelems (Usespgip vs)
in
XML.Elem("usespgip", attr "version" version, [acceptedelems])
end
-fun usespgml vs =
+fun usespgml (Usespgml vs) =
let
val version = #version vs
in
XML.Elem("usespgml", attr "version" version, [])
end
-fun pgip vs =
+fun pgip (Pgip vs) =
let
val tag = #tag vs
val class = #class vs
@@ -320,31 +320,31 @@
content)
end
-fun ready vs = XML.Elem("ready",[],[])
+fun ready (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
- | 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
+ of Cleardisplay _ => cleardisplay pgipoutput
+ | Normalresponse _ => normalresponse pgipoutput
+ | Errorresponse _ => errorresponse pgipoutput
+ | Informfileloaded _ => informfileloaded pgipoutput
+ | Informfileretracted _ => informfileretracted pgipoutput
+ | Proofstate _ => proofstate pgipoutput
+ | Metainforesponse _ => metainforesponse pgipoutput
+ | Lexicalstructure _ => lexicalstructure pgipoutput
+ | Proverinfo _ => proverinfo pgipoutput
+ | Setids _ => setids pgipoutput
+ | Addids _ => addids pgipoutput
+ | Delids _ => delids pgipoutput
+ | Hasprefs _ => hasprefs pgipoutput
+ | Prefval _ => prefval pgipoutput
+ | Idvalue _ => idvalue pgipoutput
+ | Informguise _ => informguise pgipoutput
+ | Parseresult _ => parseresult pgipoutput
+ | Usespgip _ => usespgip pgipoutput
+ | Usespgml _ => usespgml pgipoutput
+ | Pgip _ => pgip pgipoutput
+ | Ready _ => ready pgipoutput
end
--- a/src/Pure/ProofGeneral/pgip_types.ML Fri Dec 22 21:00:55 2006 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML Wed Dec 27 16:18:07 2006 +0100
@@ -115,9 +115,9 @@
(** XML utils **)
-fun has_attr attr attrs = AList.defined (op =) attrs attr
+fun has_attr (attr : string) attrs = AList.defined (op =) attrs attr
-fun get_attr_opt attr attrs = AList.lookup (op =) attrs attr
+fun get_attr_opt (attr : string) attrs = AList.lookup (op =) attrs attr
fun get_attr attr attrs =
(case get_attr_opt attr attrs of
@@ -134,7 +134,7 @@
the_default [] (Option.map (single o (pair attr_name) o f) opt_val)
*)
-val opt_attr = opt_attr_map I
+fun opt_attr attr_name = opt_attr_map I attr_name
(** Objtypes **)
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Dec 22 21:00:55 2006 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Dec 27 16:18:07 2006 +0100
@@ -446,16 +446,16 @@
(* Responses to each of the PGIP input commands.
These are programmed uniformly for extensibility. *)
-fun askpgip vs =
+fun askpgip (Askpgip vs) =
issue_pgip
(Usespgip { version = PgipIsabelle.isabelle_pgip_version_supported,
pgipelems = PgipIsabelle.accepted_inputs })
-fun askpgml vs =
+fun askpgml (Askpgml vs) =
issue_pgip
(Usespgml { version = PgipIsabelle.isabelle_pgml_version_supported })
-fun askprefs vs =
+fun askprefs (Askprefs vs) =
let
fun preference_of {name, descr, default, pgiptype, get, set } =
{ name = name, descr = SOME descr, default = SOME default,
@@ -467,7 +467,7 @@
Preferences.preferences
end
-fun askconfig vs = () (* TODO: add config response *)
+fun askconfig (Askconfig vs) = () (* TODO: add config response *)
local
fun lookuppref pref =
@@ -477,7 +477,7 @@
NONE => error ("Unknown prover preference: " ^ quote pref)
| SOME p => p
in
-fun setpref vs =
+fun setpref (Setpref vs) =
let
val name = #name vs
val value = #value vs
@@ -486,7 +486,7 @@
set value
end
-fun getpref vs =
+fun getpref (Getpref vs) =
let
val name = #name vs
val get = #get (lookuppref name)
@@ -510,14 +510,14 @@
fun pgmlsymbolsoff vs =
change print_mode (remove (op =) Symbol.xsymbolsN)
-fun dostep vs =
+fun dostep (Dostep vs) =
let
val text = #text vs
in
isarcmd text
end
-fun undostep vs =
+fun undostep (Undostep vs) =
let
val times = #times vs
in
@@ -540,7 +540,7 @@
issue_pgip (Setids {idtables =
[{context=NONE,objtype=ty,ids=[]}]}) *)
-fun 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 *)
@@ -581,7 +581,7 @@
issue_pgip (pgipfn (!lines))
end;
in
-fun showid vs =
+fun showid (Showid vs) =
let
val thyname = #thyname vs
val objtype = #objtype vs
@@ -640,7 +640,7 @@
proofpos = openproofpos })
end
-fun parsescript vs =
+fun parsescript (Parsescript vs) =
let
val text = #text vs
val systemdata = #systemdata vs
@@ -662,21 +662,21 @@
fun showctxt vs = isarcmd "print_theory" (* more useful than print_context *)
-fun searchtheorems vs =
+fun searchtheorems (Searchtheorems vs) =
let
val arg = #arg vs
in
isarcmd ("thms_containing " ^ arg)
end
-fun setlinewidth vs =
+fun setlinewidth (Setlinewidth vs) =
let
val width = #width vs
in
isarcmd ("pretty_setmargin " ^ (Int.toString width)) (* FIXME: conversion back/forth! *)
end
-fun viewdoc vs =
+fun viewdoc (Viewdoc vs) =
let
val arg = #arg vs
in
@@ -685,7 +685,7 @@
(*** Theory ***)
-fun doitem vs =
+fun doitem (Doitem vs) =
let
val text = #text vs
in
@@ -701,7 +701,7 @@
fun aborttheory vs =
isarcmd "init_toplevel"
-fun retracttheory vs =
+fun retracttheory (Retracttheory vs) =
let
val thyname = #thyname vs
in
@@ -733,7 +733,7 @@
end
end
-fun changecwd vs =
+fun changecwd (Changecwd vs) =
let
val url = #url vs
val newdir = PgipTypes.path_of_pgipurl url
@@ -741,7 +741,7 @@
changecwd_dir url
end
-fun openfile vs =
+fun openfile (Openfile vs) =
let
val url = #url vs
val filepath = PgipTypes.path_of_pgipurl url
@@ -763,7 +763,7 @@
currently_open_file := NONE)
| NONE => raise PGIP ("<closefile> when no file is open!")
-fun loadfile vs =
+fun loadfile (Loadfile vs) =
let
val url = #url vs
in
@@ -778,7 +778,7 @@
currently_open_file := NONE)
| NONE => raise PGIP ("<abortfile> when no file is open!")
-fun retractfile vs =
+fun retractfile (Retractfile vs) =
let
val url = #url vs
in
@@ -790,7 +790,7 @@
(*** System ***)
-fun systemcmd vs =
+fun systemcmd (Systemcmd vs) =
let
val arg = #arg vs
in
@@ -800,47 +800,47 @@
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_input inp = case inp
+ of Pgip.Askpgip _ => askpgip inp
+ | Pgip.Askpgml _ => askpgml inp
+ | Pgip.Askprefs _ => askprefs inp
+ | Pgip.Askconfig _ => askconfig inp
+ | Pgip.Getpref _ => getpref inp
+ | Pgip.Setpref _ => setpref inp
+ | Pgip.Proverinit _ => proverinit inp
+ | Pgip.Proverexit _ => proverexit inp
+ | Pgip.Startquiet _ => startquiet inp
+ | Pgip.Stopquiet _ => stopquiet inp
+ | Pgip.Pgmlsymbolson _ => pgmlsymbolson inp
+ | Pgip.Pgmlsymbolsoff _ => pgmlsymbolsoff inp
+ | Pgip.Dostep _ => dostep inp
+ | Pgip.Undostep _ => undostep inp
+ | Pgip.Redostep _ => redostep inp
+ | Pgip.Forget _ => error "<forget> not implemented"
+ | Pgip.Restoregoal _ => error "<restoregoal> not implemented"
+ | Pgip.Abortgoal _ => abortgoal inp
+ | Pgip.Askids _ => askids inp
+ | Pgip.Showid _ => showid inp
+ | Pgip.Askguise _ => askguise inp
+ | Pgip.Parsescript _ => parsescript inp
+ | Pgip.Showproofstate _ => showproofstate inp
+ | Pgip.Showctxt _ => showctxt inp
+ | Pgip.Searchtheorems _ => searchtheorems inp
+ | Pgip.Setlinewidth _ => setlinewidth inp
+ | Pgip.Viewdoc _ => viewdoc inp
+ | Pgip.Doitem _ => doitem inp
+ | Pgip.Undoitem _ => undoitem inp
+ | Pgip.Redoitem _ => redoitem inp
+ | Pgip.Aborttheory _ => aborttheory inp
+ | Pgip.Retracttheory _ => retracttheory inp
+ | Pgip.Loadfile _ => loadfile inp
+ | Pgip.Openfile _ => openfile inp
+ | Pgip.Closefile _ => closefile inp
+ | Pgip.Abortfile _ => abortfile inp
+ | Pgip.Retractfile _ => retractfile inp
+ | Pgip.Changecwd _ => changecwd inp
+ | Pgip.Systemcmd _ => systemcmd inp
+ | Pgip.Quitpgip _ => quitpgip inp
fun process_pgip_element pgipxml =