# HG changeset patch # User haftmann # Date 1167232687 -3600 # Node ID 8e5e2571c71660e8f455d37f5caccd4d6f1d973f # Parent 07d2a81f69c87c19b81262822eb5a91cc5fcd97b made SML/NJ happy diff -r 07d2a81f69c8 -r 8e5e2571c716 src/Pure/ProofGeneral/parsing.ML --- 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 = diff -r 07d2a81f69c8 -r 8e5e2571c716 src/Pure/ProofGeneral/pgip_output.ML --- 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 diff -r 07d2a81f69c8 -r 8e5e2571c716 src/Pure/ProofGeneral/pgip_types.ML --- 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 **) diff -r 07d2a81f69c8 -r 8e5e2571c716 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 (" 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 (" 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 " not implemented") - | Pgip.Restoregoal vs => (error " 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 " not implemented" + | Pgip.Restoregoal _ => error " 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 =