removed obsolete PGIP material;
authorwenzelm
Mon May 13 21:03:30 2013 +0200 (2013-05-13)
changeset 5196743fbd02eb9d0
parent 51966 0e18eee8c2c2
child 51968 b9b2db1e7a5e
removed obsolete PGIP material;
src/Pure/ProofGeneral/pgip_input.ML
src/Pure/ProofGeneral/pgip_isabelle.ML
src/Pure/ProofGeneral/pgip_markup.ML
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/ProofGeneral/pgml.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Mon May 13 20:35:04 2013 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,239 +0,0 @@
     1.4 -(*  Title:      Pure/ProofGeneral/pgip_input.ML
     1.5 -    Author:     David Aspinall
     1.6 -
     1.7 -PGIP abstraction: input commands.
     1.8 -*)
     1.9 -
    1.10 -signature PGIPINPUT =
    1.11 -sig
    1.12 -    (* These are the PGIP commands to which we respond. *) 
    1.13 -    datatype pgipinput = 
    1.14 -    (* protocol/prover config *)
    1.15 -      Askpgip        of { }
    1.16 -    | Askpgml        of { } 
    1.17 -    | Askconfig      of { }
    1.18 -    | Askprefs       of { }
    1.19 -    | Setpref        of { name:string, prefcategory:string option, value:string }
    1.20 -    | Getpref        of { name:string, prefcategory:string option }
    1.21 -    (* prover control *)
    1.22 -    | Proverinit     of { }
    1.23 -    | Proverexit     of { }
    1.24 -    | Setproverflag  of { flagname:string, value: bool }
    1.25 -    (* improper proof commands: control proof state *)
    1.26 -    | Dostep         of { text: string }
    1.27 -    | Undostep       of { times: int }
    1.28 -    | Redostep       of { }
    1.29 -    | Abortgoal      of { }
    1.30 -    | Forget         of { thyname: string option, name: string option, 
    1.31 -                          objtype: PgipTypes.objtype option }
    1.32 -    | Restoregoal    of { thmname : string }
    1.33 -    (* context inspection commands *)
    1.34 -    | Askids         of { url: PgipTypes.pgipurl option,
    1.35 -                          thyname: PgipTypes.objname option,
    1.36 -                          objtype: PgipTypes.objtype option }
    1.37 -    | Askrefs        of { url: PgipTypes.pgipurl option,
    1.38 -                          thyname: PgipTypes.objname option,
    1.39 -                          objtype: PgipTypes.objtype option,
    1.40 -                          name: PgipTypes.objname option }
    1.41 -    | Showid         of { thyname: PgipTypes.objname option, 
    1.42 -                          objtype: PgipTypes.objtype, 
    1.43 -                          name: PgipTypes.objname }
    1.44 -    | Askguise       of { }
    1.45 -    | Parsescript    of { text: string, location: PgipTypes.location,
    1.46 -                          systemdata: string option } 
    1.47 -    | Showproofstate of { }
    1.48 -    | Showctxt       of { }
    1.49 -    | Searchtheorems of { arg: string }
    1.50 -    | Setlinewidth   of { width: int }
    1.51 -    | Viewdoc        of { arg: string }
    1.52 -    (* improper theory-level commands *)
    1.53 -    | Doitem         of { text: string }
    1.54 -    | Undoitem       of { }
    1.55 -    | Redoitem       of { }
    1.56 -    | Aborttheory    of { }
    1.57 -    | Retracttheory  of { thyname: string }
    1.58 -    | Loadfile       of { url: PgipTypes.pgipurl }
    1.59 -    | Openfile       of { url: PgipTypes.pgipurl }
    1.60 -    | Closefile      of { }
    1.61 -    | Abortfile      of { }
    1.62 -    | Retractfile    of { url: PgipTypes.pgipurl }
    1.63 -    | Changecwd      of { url: PgipTypes.pgipurl }
    1.64 -    | Systemcmd      of { arg: string }
    1.65 -    (* unofficial escape command for debugging *)
    1.66 -    | Quitpgip       of { }
    1.67 -
    1.68 -    val input: Markup.T * XML.tree list -> pgipinput option  (* raises PGIP *)
    1.69 -end
    1.70 -
    1.71 -structure PgipInput : PGIPINPUT = 
    1.72 -struct
    1.73 -
    1.74 -open PgipTypes
    1.75 -
    1.76 -(*** PGIP input ***)
    1.77 -
    1.78 -datatype pgipinput = 
    1.79 -         (* protocol/prover config *)
    1.80 -         Askpgip        of { }
    1.81 -       | Askpgml        of { } 
    1.82 -       | Askconfig      of { }
    1.83 -       | Askprefs       of { }
    1.84 -       | Setpref        of { name:string, prefcategory:string option, value:string }
    1.85 -       | Getpref        of { name:string, prefcategory:string option }
    1.86 -       (* prover control *)
    1.87 -       | Proverinit     of { }
    1.88 -       | Proverexit     of { }
    1.89 -       | Setproverflag  of { flagname:string, value: bool }
    1.90 -       (* improper proof commands: control proof state *)
    1.91 -       | Dostep         of { text: string }
    1.92 -       | Undostep       of { times: int }
    1.93 -       | Redostep       of { }
    1.94 -       | Abortgoal      of { }
    1.95 -       | Forget         of { thyname: string option, name: string option, 
    1.96 -                             objtype: PgipTypes.objtype option }
    1.97 -       | Restoregoal    of { thmname : string }
    1.98 -       (* context inspection commands *)
    1.99 -       | Askids         of { url: PgipTypes.pgipurl option,
   1.100 -                             thyname: PgipTypes.objname option,
   1.101 -                             objtype: PgipTypes.objtype option }
   1.102 -       | Askrefs        of { url: PgipTypes.pgipurl option,
   1.103 -                             thyname: PgipTypes.objname option,
   1.104 -                             objtype: PgipTypes.objtype option,
   1.105 -                             name: PgipTypes.objname option }
   1.106 -       | Showid         of { thyname: PgipTypes.objname option, 
   1.107 -                             objtype: PgipTypes.objtype, 
   1.108 -                             name: PgipTypes.objname }
   1.109 -       | Askguise       of { }
   1.110 -       | Parsescript    of { text: string, location: location,
   1.111 -                             systemdata: string option } 
   1.112 -       | Showproofstate of { }
   1.113 -       | Showctxt       of { }
   1.114 -       | Searchtheorems of { arg: string }
   1.115 -       | Setlinewidth   of { width: int }
   1.116 -       | Viewdoc        of { arg: string }
   1.117 -       (* improper theory-level commands *)
   1.118 -       | Doitem         of { text: string }
   1.119 -       | Undoitem       of { }
   1.120 -       | Redoitem       of { }
   1.121 -       | Aborttheory    of { }
   1.122 -       | Retracttheory  of { thyname: string }
   1.123 -       | Loadfile       of { url: pgipurl }
   1.124 -       | Openfile       of { url: pgipurl }
   1.125 -       | Closefile      of { }
   1.126 -       | Abortfile      of { }
   1.127 -       | Retractfile    of { url: pgipurl }
   1.128 -       | Changecwd      of { url: pgipurl }
   1.129 -       | Systemcmd      of { arg: string }
   1.130 -       (* unofficial escape command for debugging *)
   1.131 -       | Quitpgip       of { }
   1.132 -
   1.133 -(* Extracting content from input XML elements to make a PGIPinput *)
   1.134 -local
   1.135 -
   1.136 -    val thyname_attro = get_attr_opt "thyname"
   1.137 -    val thyname_attr = get_attr "thyname"
   1.138 -    val name_attr = get_attr "name"
   1.139 -    val name_attro = get_attr_opt "name"
   1.140 -    val thmname_attr = get_attr "thmname"
   1.141 -    val flagname_attr = get_attr "flagname"
   1.142 -    val value_attr = get_attr "value"
   1.143 -
   1.144 -    fun objtype_attro attrs = if has_attr "objtype" attrs then
   1.145 -                                  SOME (objtype_of_attrs attrs)
   1.146 -                              else NONE
   1.147 -
   1.148 -    fun pgipurl_attro attrs = if has_attr "url" attrs then
   1.149 -                                  SOME (pgipurl_of_attrs attrs)
   1.150 -                              else NONE
   1.151 -
   1.152 -    val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
   1.153 -    val prefcat_attr = get_attr_opt "prefcategory"
   1.154 -
   1.155 -    fun xmltext (XML.Text text :: ts) = text ^ xmltext ts
   1.156 -      | xmltext [] = ""
   1.157 -      | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
   1.158 -
   1.159 -    exception Unknown
   1.160 -    exception NoAction
   1.161 -in
   1.162 -
   1.163 -(* Return a valid PGIP input command.
   1.164 -   Raise PGIP exception for invalid data.
   1.165 -   Return NONE for unknown/unhandled commands. 
   1.166 -*)
   1.167 -fun input ((elem, attrs), data) =
   1.168 -SOME 
   1.169 - (case elem of 
   1.170 -     "askpgip"        => Askpgip { }
   1.171 -   | "askpgml"        => Askpgml { }
   1.172 -   | "askconfig"      => Askconfig { }
   1.173 -   (* proverconfig *)
   1.174 -   | "askprefs"       => Askprefs { }
   1.175 -   | "getpref"        => Getpref { name = name_attr attrs, 
   1.176 -                                   prefcategory = prefcat_attr attrs }
   1.177 -   | "setpref"        => Setpref { name = name_attr attrs, 
   1.178 -                                   prefcategory = prefcat_attr attrs,
   1.179 -                                   value = xmltext data }
   1.180 -   (* provercontrol *)
   1.181 -   | "proverinit"     => Proverinit { }
   1.182 -   | "proverexit"     => Proverexit { }
   1.183 -   | "setproverflag"  => Setproverflag { flagname = flagname_attr attrs,
   1.184 -                                         value = read_pgipbool (value_attr attrs) }
   1.185 -   (* improperproofcmd: improper commands not in script *)
   1.186 -   | "dostep"         => Dostep    { text = xmltext data }
   1.187 -   | "undostep"       => Undostep  { times = times_attr attrs }
   1.188 -   | "redostep"       => Redostep  { } 
   1.189 -   | "abortgoal"      => Abortgoal { }
   1.190 -   | "forget"         => Forget { thyname = thyname_attro attrs, 
   1.191 -                                  name = name_attro attrs,
   1.192 -                                  objtype = objtype_attro attrs }
   1.193 -   | "restoregoal"    => Restoregoal { thmname = thmname_attr attrs}
   1.194 -   (* proofctxt: improper commands *)
   1.195 -   | "askids"         => Askids { url = pgipurl_attro attrs,
   1.196 -                                  thyname = thyname_attro attrs, 
   1.197 -                                  objtype = objtype_attro attrs }
   1.198 -   | "askrefs"        => Askrefs { url = pgipurl_attro attrs,
   1.199 -                                   thyname = thyname_attro attrs, 
   1.200 -                                   objtype = objtype_attro attrs,
   1.201 -                                   name = name_attro attrs }
   1.202 -   | "showid"         => Showid { thyname = thyname_attro attrs,
   1.203 -                                  objtype = objtype_of_attrs attrs,
   1.204 -                                  name = name_attr attrs }
   1.205 -   | "askguise"       => Askguise { }
   1.206 -   | "parsescript"    => Parsescript { text = (xmltext data),
   1.207 -                                       systemdata = get_attr_opt "systemdata" attrs,
   1.208 -                                       location = location_of_attrs attrs }
   1.209 -   | "showproofstate" => Showproofstate { }
   1.210 -   | "showctxt"       => Showctxt { }
   1.211 -   | "searchtheorems" => Searchtheorems { arg = xmltext data }
   1.212 -   | "setlinewidth"   => Setlinewidth   { width = read_pgipnat (xmltext data) }
   1.213 -   | "viewdoc"        => Viewdoc { arg = xmltext data }
   1.214 -   (* improperfilecmd: theory-level commands not in script *)
   1.215 -   | "doitem"         => Doitem  { text = xmltext data }
   1.216 -   | "undoitem"       => Undoitem { }
   1.217 -   | "redoitem"       => Redoitem { }
   1.218 -   | "aborttheory"    => Aborttheory { }
   1.219 -   | "retracttheory"  => Retracttheory { thyname = thyname_attr attrs }
   1.220 -   | "loadfile"       => Loadfile { url = pgipurl_of_attrs attrs }
   1.221 -   | "openfile"       => Openfile { url = pgipurl_of_attrs attrs }
   1.222 -   | "closefile"      => Closefile { }
   1.223 -   | "abortfile"      => Abortfile { }
   1.224 -   | "retractfile"    => Retractfile { url = pgipurl_of_attrs attrs }
   1.225 -   | "changecwd"      => Changecwd { url = pgipurl_of_attrs attrs }
   1.226 -   | "systemcmd"      => Systemcmd { arg = xmltext data }
   1.227 -   (* unofficial command for debugging *)
   1.228 -   | "quitpgip" => Quitpgip { }
   1.229 -
   1.230 -   (* We allow sending proper document markup too; we map it back to dostep   *)
   1.231 -   (* and strip out metainfo elements. Markup correctness isn't checked: this *)
   1.232 -   (* is a compatibility measure to make it easy for interfaces.              *)
   1.233 -   | x => if member (op =) PgipMarkup.doc_markup_elements x then
   1.234 -              if member (op =) PgipMarkup.doc_markup_elements_ignored x then
   1.235 -                  raise NoAction
   1.236 -              else 
   1.237 -                  Dostep { text = xmltext data } (* could separate out Doitem too *)
   1.238 -          else raise Unknown) 
   1.239 -    handle Unknown => NONE | NoAction => NONE
   1.240 -end
   1.241 -
   1.242 -end
     2.1 --- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Mon May 13 20:35:04 2013 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,111 +0,0 @@
     2.4 -(*  Title:      Pure/ProofGeneral/pgip_isabelle.ML
     2.5 -    Author:     David Aspinall
     2.6 -
     2.7 -Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.
     2.8 -*)
     2.9 -
    2.10 -signature PGIP_ISABELLE =
    2.11 -sig
    2.12 -    val isabelle_pgml_version_supported : string
    2.13 -    val isabelle_pgip_version_supported : string
    2.14 -    val systemid : string
    2.15 -    val accepted_inputs : (string * bool * (string list)) list
    2.16 -
    2.17 -    val location_of_position : Position.T -> PgipTypes.location
    2.18 -
    2.19 -    (* Additional types of objects in Isar scripts *)
    2.20 -
    2.21 -    val ObjTheoryBody : PgipTypes.objtype
    2.22 -    val ObjTheoryDecl : PgipTypes.objtype
    2.23 -    val ObjTheoryBodySubsection : PgipTypes.objtype
    2.24 -    val ObjProofBody : PgipTypes.objtype
    2.25 -    val ObjFormalComment : PgipTypes.objtype
    2.26 -    val ObjClass : PgipTypes.objtype
    2.27 -    val ObjTheoremSet : PgipTypes.objtype
    2.28 -    val ObjOracle : PgipTypes.objtype
    2.29 -    val ObjLocale : PgipTypes.objtype
    2.30 -
    2.31 -end
    2.32 -
    2.33 -structure PgipIsabelle : PGIP_ISABELLE =
    2.34 -struct
    2.35 -
    2.36 -val isabelle_pgml_version_supported = "2.0";
    2.37 -val isabelle_pgip_version_supported = "2.0"
    2.38 -val systemid = "Isabelle"
    2.39 -
    2.40 -
    2.41 -(** Accepted commands **)
    2.42 -
    2.43 -local
    2.44 -
    2.45 -    (* These element names are a subset of those in pgip_input.ML.
    2.46 -       They must be handled in proof_general_pgip.ML/process_pgip_element. *)
    2.47 -
    2.48 -    val accepted_names =
    2.49 -    (* not implemented: "askconfig", "forget", "restoregoal" *)
    2.50 -    ["askpgip","askpgml","askprefs","getpref","setpref",
    2.51 -     "proverinit","proverexit","startquiet","stopquiet",
    2.52 -     "pgmlsymbolson", "pgmlsymbolsoff",
    2.53 -     "dostep", "undostep", "redostep", "abortgoal",
    2.54 -     "askids", "showid", "askguise",
    2.55 -     "parsescript",
    2.56 -     "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
    2.57 -     "doitem", "undoitem", "redoitem", "abortheory",
    2.58 -     "retracttheory", "loadfile", "openfile", "closefile",
    2.59 -     "abortfile", "retractfile", "changecwd", "systemcmd"];
    2.60 -
    2.61 -    fun element_async p =
    2.62 -        false (* single threaded only *)
    2.63 -
    2.64 -    fun supported_optional_attrs p = (case p of
    2.65 -                                          "undostep" => ["times"]
    2.66 -                                        (* TODO: we could probably extend these too:
    2.67 -                                        | "redostep" => ["times"]
    2.68 -                                        | "undoitem" => ["times"]
    2.69 -                                        | "redoitem" => ["times"] *)
    2.70 -                                        | _ => [])
    2.71 -in
    2.72 -val accepted_inputs =
    2.73 -    (map (fn p=> (p, element_async p, supported_optional_attrs p))
    2.74 -         accepted_names);
    2.75 -end
    2.76 -
    2.77 -
    2.78 -fun location_of_position pos =
    2.79 -    let val line = Position.line_of pos
    2.80 -        val (url,descr) =
    2.81 -            (case Position.file_of pos of
    2.82 -               NONE => (NONE, NONE)
    2.83 -             | SOME fname =>
    2.84 -               let val path = Path.explode fname in
    2.85 -                 if File.exists path
    2.86 -                 then (SOME (PgipTypes.pgipurl_of_path path), NONE)
    2.87 -                 else (NONE, SOME fname)
    2.88 -               end);
    2.89 -    in
    2.90 -        { descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
    2.91 -    end
    2.92 -
    2.93 -
    2.94 -val [ObjTheoryBody,
    2.95 -     ObjTheoryDecl,
    2.96 -     ObjTheoryBodySubsection,
    2.97 -     ObjProofBody,
    2.98 -     ObjFormalComment,
    2.99 -     ObjClass,
   2.100 -     ObjTheoremSet,
   2.101 -     ObjOracle,
   2.102 -     ObjLocale] =
   2.103 -    map PgipTypes.ObjOther
   2.104 -        ["theory body",
   2.105 -         "theory declaration",
   2.106 -         "theory subsection",
   2.107 -         "proof body",
   2.108 -         "formal comment",
   2.109 -         "class",
   2.110 -         "theorem set declaration",
   2.111 -         "oracle",
   2.112 -         "locale"];
   2.113 -
   2.114 -end
     3.1 --- a/src/Pure/ProofGeneral/pgip_markup.ML	Mon May 13 20:35:04 2013 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,213 +0,0 @@
     3.4 -(*  Title:      Pure/ProofGeneral/pgip_markup.ML
     3.5 -    Author:     David Aspinall
     3.6 -
     3.7 -PGIP abstraction: document markup for proof scripts (in progress).
     3.8 -*)
     3.9 -
    3.10 -signature PGIPMARKUP =
    3.11 -sig
    3.12 -  (* Generic markup on sequential, non-overlapping pieces of proof text *)
    3.13 -  datatype pgipdoc =
    3.14 -    Openblock     of { metavarid: string option, name: string option,
    3.15 -                       objtype: PgipTypes.objtype option }
    3.16 -  | Closeblock    of { }
    3.17 -  | Opentheory    of { thyname: string option, parentnames: string list , text: string}
    3.18 -  | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
    3.19 -  | Closetheory   of { text: string }
    3.20 -  | Opengoal      of { thmname: string option, text: string }
    3.21 -  | Proofstep     of { text: string }
    3.22 -  | Closegoal     of { text: string }
    3.23 -  | Giveupgoal    of { text: string }
    3.24 -  | Postponegoal  of { text: string }
    3.25 -  | Comment       of { text: string }
    3.26 -  | Doccomment    of { text: string }
    3.27 -  | Whitespace    of { text: string }
    3.28 -  | Spuriouscmd   of { text: string }
    3.29 -  | Badcmd        of { text: string }
    3.30 -  | Unparseable   of { text: string }
    3.31 -  | Metainfo      of { name: string option, text: string }
    3.32 -  (* Last three for PGIP literate markup only: *)
    3.33 -  | Litcomment    of { format: string option, content: XML.tree list }
    3.34 -  | Showcode      of { show: bool }
    3.35 -  | Setformat     of { format: string }
    3.36 -
    3.37 -  type pgipdocument = pgipdoc list
    3.38 -  type pgip_parser  = string -> pgipdocument       (* system must provide a parser P *)
    3.39 -  val unparse_doc : pgipdocument -> string list    (* s.t. unparse (P x) = x         *)
    3.40 -  val output_doc : pgipdocument -> XML.tree list
    3.41 -  val doc_markup_elements : string list            (* used in pgip_input *)
    3.42 -  val doc_markup_elements_ignored : string list    (* used in pgip_input *)
    3.43 -end
    3.44 -
    3.45 -
    3.46 -structure PgipMarkup : PGIPMARKUP =
    3.47 -struct
    3.48 -   open PgipTypes
    3.49 -
    3.50 -(* PGIP 3 idea: replace opentheory, opengoal, etc. by just openblock with corresponding objtype? *)
    3.51 -  datatype pgipdoc =
    3.52 -    Openblock     of { metavarid: string option, name: string option,
    3.53 -                       objtype: PgipTypes.objtype option }
    3.54 -  | Closeblock    of { }
    3.55 -  | Opentheory    of { thyname: string option, parentnames: string list, text: string}
    3.56 -  | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
    3.57 -  | Closetheory   of { text: string }
    3.58 -  | Opengoal      of { thmname: string option, text: string }
    3.59 -  | Proofstep     of { text: string }
    3.60 -  | Closegoal     of { text: string }
    3.61 -  | Giveupgoal    of { text: string }
    3.62 -  | Postponegoal  of { text: string }
    3.63 -  | Comment       of { text: string }
    3.64 -  | Doccomment    of { text: string }
    3.65 -  | Whitespace    of { text: string }
    3.66 -  | Spuriouscmd   of { text: string }
    3.67 -  | Badcmd        of { text: string }
    3.68 -  | Unparseable   of { text: string }
    3.69 -  | Metainfo      of { name: string option, text: string }
    3.70 -  | Litcomment    of { format: string option, content: XML.tree list }
    3.71 -  | Showcode      of { show: bool }
    3.72 -  | Setformat     of { format: string }
    3.73 -
    3.74 -  type pgipdocument = pgipdoc list
    3.75 -  type pgip_parser  = string -> pgipdocument
    3.76 -
    3.77 -   fun xml_of docelt =
    3.78 -       case docelt of
    3.79 -
    3.80 -           Openblock vs  =>
    3.81 -           XML.Elem(("openblock", opt_attr "name" (#metavarid vs) @
    3.82 -                                  opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
    3.83 -                                  opt_attr "metavarid" (#metavarid vs)),
    3.84 -                    [])
    3.85 -
    3.86 -         | Closeblock _ =>
    3.87 -           XML.Elem(("closeblock", []), [])
    3.88 -
    3.89 -         | Opentheory vs  =>
    3.90 -           XML.Elem(("opentheory",
    3.91 -                    opt_attr "thyname" (#thyname vs) @
    3.92 -                    opt_attr "parentnames"
    3.93 -                             (case (#parentnames vs)
    3.94 -                               of [] => NONE
    3.95 -                                | ps => SOME (space_implode ";" ps))),
    3.96 -                    [XML.Text (#text vs)])
    3.97 -
    3.98 -         | Theoryitem vs =>
    3.99 -           XML.Elem(("theoryitem",
   3.100 -                    opt_attr "name" (#name vs) @
   3.101 -                    opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs)),
   3.102 -                    [XML.Text (#text vs)])
   3.103 -
   3.104 -         | Closetheory vs =>
   3.105 -           XML.Elem(("closetheory", []), [XML.Text (#text vs)])
   3.106 -
   3.107 -         | Opengoal vs =>
   3.108 -           XML.Elem(("opengoal",
   3.109 -                    opt_attr "thmname" (#thmname vs)),
   3.110 -                    [XML.Text (#text vs)])
   3.111 -
   3.112 -         | Proofstep vs =>
   3.113 -           XML.Elem(("proofstep", []), [XML.Text (#text vs)])
   3.114 -
   3.115 -         | Closegoal vs =>
   3.116 -           XML.Elem(("closegoal", []), [XML.Text (#text vs)])
   3.117 -
   3.118 -         | Giveupgoal vs =>
   3.119 -           XML.Elem(("giveupgoal", []), [XML.Text (#text vs)])
   3.120 -
   3.121 -         | Postponegoal vs =>
   3.122 -           XML.Elem(("postponegoal", []), [XML.Text (#text vs)])
   3.123 -
   3.124 -         | Comment vs =>
   3.125 -           XML.Elem(("comment", []), [XML.Text (#text vs)])
   3.126 -
   3.127 -         | Whitespace vs =>
   3.128 -           XML.Elem(("whitespace", []), [XML.Text (#text vs)])
   3.129 -
   3.130 -         | Doccomment vs =>
   3.131 -           XML.Elem(("doccomment", []), [XML.Text (#text vs)])
   3.132 -
   3.133 -         | Spuriouscmd vs =>
   3.134 -           XML.Elem(("spuriouscmd", []), [XML.Text (#text vs)])
   3.135 -
   3.136 -         | Badcmd vs =>
   3.137 -           XML.Elem(("badcmd", []), [XML.Text (#text vs)])
   3.138 -
   3.139 -         | Unparseable vs =>
   3.140 -           XML.Elem(("unparseable", []), [XML.Text (#text vs)])
   3.141 -
   3.142 -         | Metainfo vs =>
   3.143 -           XML.Elem(("metainfo", opt_attr "name" (#name vs)),
   3.144 -                    [XML.Text (#text vs)])
   3.145 -
   3.146 -         | Litcomment vs =>
   3.147 -           XML.Elem(("litcomment", opt_attr "format" (#format vs)),
   3.148 -                   #content vs)
   3.149 -
   3.150 -         | Showcode vs =>
   3.151 -           XML.Elem(("showcode",
   3.152 -                    attr "show" (PgipTypes.bool_to_pgstring (#show vs))), [])
   3.153 -
   3.154 -         | Setformat vs =>
   3.155 -           XML.Elem(("setformat", attr "format" (#format vs)), [])
   3.156 -
   3.157 -   val output_doc = map xml_of
   3.158 -
   3.159 -   fun unparse_elt docelt =
   3.160 -   case docelt of
   3.161 -       Openblock _ => ""
   3.162 -     | Closeblock _ => ""
   3.163 -     | Opentheory vs => #text vs
   3.164 -     | Theoryitem vs => #text vs
   3.165 -     | Closetheory vs => #text vs
   3.166 -     | Opengoal vs => #text vs
   3.167 -     | Proofstep vs => #text vs
   3.168 -     | Closegoal vs => #text vs
   3.169 -     | Giveupgoal vs => #text vs
   3.170 -     | Postponegoal vs => #text vs
   3.171 -     | Comment vs => #text vs
   3.172 -     | Doccomment vs => #text vs
   3.173 -     | Whitespace vs => #text vs
   3.174 -     | Spuriouscmd vs => #text vs
   3.175 -     | Badcmd vs => #text vs
   3.176 -     | Unparseable vs => #text vs
   3.177 -     | Metainfo vs => #text vs
   3.178 -     | _ => ""
   3.179 -
   3.180 -
   3.181 -   val unparse_doc = map unparse_elt
   3.182 -
   3.183 -
   3.184 -   (* Names of all PGIP document markup elements *)
   3.185 -   val doc_markup_elements =
   3.186 -       ["openblock",
   3.187 -        "closeblock",
   3.188 -        "opentheory",
   3.189 -        "theoryitem",
   3.190 -        "closetheory",
   3.191 -        "opengoal",
   3.192 -        "proofstep",
   3.193 -        "closegoal",
   3.194 -        "giveupgoal",
   3.195 -        "postponegoal",
   3.196 -        "comment",
   3.197 -        "doccomment",
   3.198 -        "whitespace",
   3.199 -        "spuriouscmd",
   3.200 -        "badcmd",
   3.201 -        (* the prover shouldn't really receive the next ones,
   3.202 -           but we include them here so that they are harmlessly
   3.203 -           ignored. *)
   3.204 -        "unparseable",
   3.205 -        "metainfo",
   3.206 -        (* Broker document format *)
   3.207 -        "litcomment",
   3.208 -        "showcode",
   3.209 -        "setformat"]
   3.210 -
   3.211 -   (* non-document/empty text, must be ignored *)
   3.212 -   val doc_markup_elements_ignored =
   3.213 -       [ "metainfo", "openblock", "closeblock",
   3.214 -         "litcomment", "showcode", "setformat" ]
   3.215 -
   3.216 -end;
     4.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Mon May 13 20:35:04 2013 +0200
     4.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Mon May 13 21:03:30 2013 +0200
     4.3 @@ -6,326 +6,44 @@
     4.4  
     4.5  signature PGIPOUTPUT =
     4.6  sig
     4.7 -    (* These are the PGIP messages which the prover emits. *) 
     4.8 -    datatype pgipoutput = 
     4.9 -      Normalresponse      of { content: XML.tree list }
    4.10 -    | Errorresponse       of { fatality: PgipTypes.fatality, 
    4.11 -                               location: PgipTypes.location option, 
    4.12 -                               content: XML.tree list }
    4.13 -    | Informfileloaded    of { url: PgipTypes.pgipurl, completed: bool }
    4.14 -    | Informfileoutdated  of { url: PgipTypes.pgipurl, completed: bool }
    4.15 -    | Informfileretracted of { url: PgipTypes.pgipurl, completed: bool }
    4.16 -    | Metainforesponse    of { attrs: XML.attributes, 
    4.17 -                               content: XML.tree list }
    4.18 -    | Lexicalstructure    of { content: XML.tree list }
    4.19 -    | Proverinfo          of { name: string, 
    4.20 -                               version: string, 
    4.21 -                               instance: string,
    4.22 -                               descr: string, 
    4.23 -                               url: Url.T, 
    4.24 -                               filenameextns: string }
    4.25 -    | Setids              of { idtables: PgipTypes.idtable list  }
    4.26 -    | Delids              of { idtables: PgipTypes.idtable list }
    4.27 -    | Addids              of { idtables: PgipTypes.idtable list }
    4.28 -    | Hasprefs            of { prefcategory: string option, 
    4.29 +    datatype pgipoutput =
    4.30 +      Hasprefs            of { prefcategory: string option, 
    4.31                                 prefs: PgipTypes.preference list }
    4.32 -    | Prefval             of { name: string, value: string }
    4.33 -    | Setrefs             of { url: PgipTypes.pgipurl option,
    4.34 -                               thyname: PgipTypes.objname option,
    4.35 -                               objtype: PgipTypes.objtype option,
    4.36 -                               name: PgipTypes.objname option,
    4.37 -                               idtables: PgipTypes.idtable list,
    4.38 -                               fileurls : PgipTypes.pgipurl list }
    4.39 -    | Idvalue             of { thyname: PgipTypes.objname option,
    4.40 -                               objtype: PgipTypes.objtype, 
    4.41 -                               name: PgipTypes.objname, 
    4.42 -                               text: XML.tree list }
    4.43 -    | Informguise         of { file : PgipTypes.pgipurl option,  
    4.44 -                               theory: PgipTypes.objname option, 
    4.45 -                               theorem: PgipTypes.objname option, 
    4.46 -                               proofpos: int option }
    4.47 -    | Parseresult         of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument, 
    4.48 -                               errs: XML.tree list } (* errs to become PGML *)
    4.49 -    | Usespgip            of { version: string, 
    4.50 -                               pgipelems: (string * bool * string list) list }
    4.51 -    | Usespgml            of { version: string }
    4.52 -    | Pgip                of { tag: string option, 
    4.53 -                               class: string, 
    4.54 -                               seq: int, id: string, 
    4.55 +    | Pgip                of { tag: string option,
    4.56 +                               class: string,
    4.57 +                               seq: int, id: string,
    4.58                                 destid: string option,
    4.59                                 refid: string option,
    4.60                                 refseq: int option,
    4.61                                 content: XML.tree list }
    4.62 -    | Ready               of { }
    4.63  
    4.64 -    val output : pgipoutput -> XML.tree                                  
    4.65 +    val output : pgipoutput -> XML.tree
    4.66  end
    4.67  
    4.68  structure PgipOutput : PGIPOUTPUT =
    4.69  struct
    4.70 -open PgipTypes
    4.71  
    4.72 -datatype pgipoutput = 
    4.73 -         Normalresponse      of { content: XML.tree list }
    4.74 -       | Errorresponse       of { fatality: fatality, 
    4.75 -                                  location: location option, 
    4.76 -                                  content: XML.tree list }
    4.77 -       | Informfileloaded    of { url: Path.T, completed: bool }
    4.78 -       | Informfileoutdated  of { url: Path.T, completed: bool }
    4.79 -       | Informfileretracted of { url: Path.T, completed: bool }
    4.80 -       | Metainforesponse    of { attrs: XML.attributes, content: XML.tree list }
    4.81 -       | Lexicalstructure    of { content: XML.tree list }
    4.82 -       | Proverinfo          of { name: string, version: string, instance: string,
    4.83 -                                  descr: string, url: Url.T, filenameextns: string }
    4.84 -       | Setids              of { idtables: PgipTypes.idtable list  }
    4.85 -       | Delids              of { idtables: PgipTypes.idtable list }
    4.86 -       | Addids              of { idtables: PgipTypes.idtable list }
    4.87 -       | Hasprefs            of { prefcategory: string option, prefs: preference list }
    4.88 -       | Prefval             of { name: string, value: string }
    4.89 -       | Idvalue             of { thyname: PgipTypes.objname option,
    4.90 -                                  objtype: PgipTypes.objtype, 
    4.91 -                                  name: PgipTypes.objname, 
    4.92 -                                  text: XML.tree list }
    4.93 -       | Setrefs             of { url: PgipTypes.pgipurl option,
    4.94 -                                  thyname: PgipTypes.objname option,
    4.95 -                                  objtype: PgipTypes.objtype option,
    4.96 -                                  name: PgipTypes.objname option,
    4.97 -                                  idtables: PgipTypes.idtable list,
    4.98 -                                  fileurls : PgipTypes.pgipurl list }
    4.99 -       | Informguise         of { file : PgipTypes.pgipurl option,  
   4.100 -                                  theory: PgipTypes.objname option, 
   4.101 -                                  theorem: PgipTypes.objname option, 
   4.102 -                                  proofpos: int option }
   4.103 -       | Parseresult         of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
   4.104 -                                  errs: XML.tree list } (* errs to become PGML *)
   4.105 -       | Usespgip            of { version: string, 
   4.106 -                                  pgipelems: (string * bool * string list) list }
   4.107 -       | Usespgml            of { version: string }
   4.108 -       | Pgip                of { tag: string option, 
   4.109 -                                  class: string, 
   4.110 -                                  seq: int, id: string, 
   4.111 +datatype pgipoutput =
   4.112 +         Hasprefs            of { prefcategory: string option, 
   4.113 +                                  prefs: PgipTypes.preference list }
   4.114 +  |      Pgip                of { tag: string option,
   4.115 +                                  class: string,
   4.116 +                                  seq: int, id: string,
   4.117                                    destid: string option,
   4.118                                    refid: string option,
   4.119                                    refseq: int option,
   4.120                                    content: XML.tree list }
   4.121 -       | Ready               of { }
   4.122  
   4.123 -
   4.124 -(* Construct output XML messages *)
   4.125 -
   4.126 -fun normalresponse (Normalresponse vs) =
   4.127 -    let 
   4.128 -        val content = #content vs
   4.129 -    in
   4.130 -        XML.Elem (("normalresponse", []), content)
   4.131 -    end
   4.132 -
   4.133 -fun errorresponse (Errorresponse vs) =
   4.134 -    let 
   4.135 -        val fatality = #fatality vs
   4.136 -        val location = #location vs
   4.137 -        val content = #content vs
   4.138 -    in
   4.139 -        XML.Elem (("errorresponse",
   4.140 -                 attrs_of_fatality fatality @
   4.141 -                 these (Option.map attrs_of_location location)),
   4.142 -                 content)
   4.143 -    end
   4.144 -
   4.145 -fun informfileloaded (Informfileloaded vs) =
   4.146 -    let 
   4.147 -        val url = #url vs
   4.148 -        val completed = #completed vs
   4.149 -    in
   4.150 -        XML.Elem (("informfileloaded", 
   4.151 -                  attrs_of_pgipurl url @ 
   4.152 -                  (attr "completed" (PgipTypes.bool_to_pgstring completed))),
   4.153 -                  [])
   4.154 -    end
   4.155 -
   4.156 -fun informfileoutdated (Informfileoutdated vs) =
   4.157 -    let 
   4.158 -        val url = #url vs
   4.159 -        val completed = #completed vs
   4.160 -    in
   4.161 -        XML.Elem (("informfileoutdated", 
   4.162 -                  attrs_of_pgipurl url @ 
   4.163 -                  (attr "completed" (PgipTypes.bool_to_pgstring completed))),
   4.164 -                  [])
   4.165 -    end
   4.166 -
   4.167 -fun informfileretracted (Informfileretracted vs) =
   4.168 +fun output (Hasprefs vs) =
   4.169      let 
   4.170 -        val url = #url vs
   4.171 -        val completed = #completed vs
   4.172 -    in
   4.173 -        XML.Elem (("informfileretracted", 
   4.174 -                  attrs_of_pgipurl url @ 
   4.175 -                  (attr "completed" (PgipTypes.bool_to_pgstring completed))),
   4.176 -                  [])
   4.177 -    end
   4.178 -
   4.179 -fun metainforesponse (Metainforesponse vs) =
   4.180 -    let 
   4.181 -        val attrs = #attrs vs
   4.182 -        val content = #content vs
   4.183 -    in
   4.184 -        XML.Elem (("metainforesponse", attrs), content)
   4.185 -    end
   4.186 -
   4.187 -fun lexicalstructure (Lexicalstructure vs) =
   4.188 -    let
   4.189 -        val content = #content vs
   4.190 -    in
   4.191 -        XML.Elem (("lexicalstructure", []), content)
   4.192 +        val prefcategory = #prefcategory vs
   4.193 +        val prefs = #prefs vs
   4.194 +    in 
   4.195 +        XML.Elem (("hasprefs", PgipTypes.opt_attr "prefcategory" prefcategory),
   4.196 +          map PgipTypes.haspref prefs)
   4.197      end
   4.198 -
   4.199 -fun proverinfo (Proverinfo vs) =
   4.200 -    let
   4.201 -        val name = #name vs
   4.202 -        val version = #version vs
   4.203 -        val instance = #instance vs
   4.204 -        val descr = #descr vs
   4.205 -        val url = #url vs
   4.206 -        val filenameextns = #filenameextns vs
   4.207 -    in 
   4.208 -        XML.Elem (("proverinfo",
   4.209 -                 [("name", name),
   4.210 -                  ("version", version),
   4.211 -                  ("instance", instance), 
   4.212 -                  ("descr", descr),
   4.213 -                  ("url", Url.implode url),
   4.214 -                  ("filenameextns", filenameextns)]),
   4.215 -                 [])
   4.216 -    end
   4.217 -
   4.218 -fun setids (Setids vs) =
   4.219 -    let
   4.220 -        val idtables = #idtables vs
   4.221 -    in
   4.222 -        XML.Elem (("setids", []), map idtable_to_xml idtables)
   4.223 -    end
   4.224 -
   4.225 -fun setrefs (Setrefs vs) =
   4.226 +  | output (Pgip vs) =
   4.227      let
   4.228 -        val url = #url vs
   4.229 -        val thyname = #thyname vs
   4.230 -        val objtype = #objtype vs
   4.231 -        val name = #name vs
   4.232 -        val idtables = #idtables vs
   4.233 -        val fileurls = #fileurls vs
   4.234 -        fun fileurl_to_xml url = XML.Elem (("fileurl", attrs_of_pgipurl url), [])
   4.235 -    in
   4.236 -        XML.Elem (("setrefs",
   4.237 -                  (the_default [] (Option.map attrs_of_pgipurl url)) @ 
   4.238 -                  (the_default [] (Option.map attrs_of_objtype objtype)) @
   4.239 -                  (opt_attr "thyname" thyname) @
   4.240 -                  (opt_attr "name" name)),
   4.241 -                  (map idtable_to_xml idtables) @ 
   4.242 -                  (map fileurl_to_xml fileurls))
   4.243 -    end
   4.244 -
   4.245 -fun addids (Addids vs) =
   4.246 -    let
   4.247 -        val idtables = #idtables vs
   4.248 -    in
   4.249 -        XML.Elem (("addids", []), map idtable_to_xml idtables)
   4.250 -    end
   4.251 -
   4.252 -fun delids (Delids vs) =
   4.253 -    let
   4.254 -        val idtables = #idtables vs
   4.255 -    in
   4.256 -        XML.Elem (("delids", []), map idtable_to_xml idtables)
   4.257 -    end
   4.258 -
   4.259 -fun hasprefs (Hasprefs vs) =
   4.260 -  let 
   4.261 -      val prefcategory = #prefcategory vs
   4.262 -      val prefs = #prefs vs
   4.263 -  in 
   4.264 -      XML.Elem (("hasprefs", opt_attr "prefcategory" prefcategory), map haspref prefs)
   4.265 -  end
   4.266 -
   4.267 -fun prefval (Prefval vs) =
   4.268 -    let 
   4.269 -        val name = #name vs
   4.270 -        val value = #value vs
   4.271 -    in
   4.272 -        XML.Elem (("prefval", attr "name" name), [XML.Text value])
   4.273 -    end 
   4.274 -
   4.275 -fun idvalue (Idvalue vs) =
   4.276 -    let 
   4.277 -        val objtype_attrs = attrs_of_objtype (#objtype vs)
   4.278 -        val thyname = #thyname vs
   4.279 -        val name = #name vs
   4.280 -        val text = #text vs
   4.281 -    in
   4.282 -        XML.Elem (("idvalue", 
   4.283 -                 objtype_attrs @
   4.284 -                 (opt_attr "thyname" thyname) @
   4.285 -                 attr "name" name),
   4.286 -                 text)
   4.287 -    end
   4.288 -
   4.289 -fun informguise (Informguise vs) =
   4.290 -  let
   4.291 -      val file = #file vs
   4.292 -      val theory = #theory vs
   4.293 -      val theorem = #theorem vs
   4.294 -      val proofpos = #proofpos vs
   4.295 -
   4.296 -      fun elto nm attrfn xo = case xo of NONE => [] | SOME x => [XML.Elem ((nm, attrfn x), [])]
   4.297 -
   4.298 -      val guisefile = elto "guisefile" attrs_of_pgipurl file
   4.299 -      val guisetheory = elto "guisetheory" (single o (pair "thyname")) theory
   4.300 -      val guiseproof = elto "guiseproof" 
   4.301 -                            (fn thm=>(attr "thmname" thm) @
   4.302 -                                     (opt_attr "proofpos" (Option.map string_of_int proofpos))) theorem
   4.303 -  in 
   4.304 -      XML.Elem (("informguise", []), guisefile @ guisetheory @ guiseproof)
   4.305 -  end
   4.306 -
   4.307 -fun parseresult (Parseresult vs) =
   4.308 -    let
   4.309 -        val attrs = #attrs vs
   4.310 -        val doc = #doc vs
   4.311 -        val errs = #errs vs
   4.312 -        val xmldoc = PgipMarkup.output_doc doc
   4.313 -    in 
   4.314 -        XML.Elem (("parseresult", attrs), errs @ xmldoc)
   4.315 -    end
   4.316 -
   4.317 -fun acceptedpgipelems (Usespgip vs) = 
   4.318 -    let
   4.319 -        val pgipelems = #pgipelems vs
   4.320 -        fun async_attrs b = if b then attr "async" "true" else []
   4.321 -        fun attrs_attrs attrs = if attrs=[] then [] else attr "attributes" (space_implode "," attrs)
   4.322 -        fun singlepgipelem (e,async,attrs) = 
   4.323 -            XML.Elem (("pgipelem", async_attrs async @ attrs_attrs attrs), [XML.Text e])
   4.324 -                                                      
   4.325 -    in
   4.326 -        XML.Elem (("acceptedpgipelems", []), map singlepgipelem pgipelems)
   4.327 -    end
   4.328 -
   4.329 -fun usespgip (Usespgip vs) =
   4.330 -    let
   4.331 -        val version = #version vs
   4.332 -        val acceptedelems = acceptedpgipelems (Usespgip vs)
   4.333 -    in 
   4.334 -        XML.Elem (("usespgip", attr "version" version), [acceptedelems])
   4.335 -    end
   4.336 -
   4.337 -fun usespgml (Usespgml vs) =
   4.338 -    let
   4.339 -        val version = #version vs
   4.340 -    in 
   4.341 -        XML.Elem (("usespgml", attr "version" version), [])
   4.342 -    end
   4.343 -
   4.344 -fun pgip (Pgip vs) =
   4.345 -    let 
   4.346          val tag = #tag vs
   4.347          val class = #class vs
   4.348          val seq = #seq vs
   4.349 @@ -336,41 +54,15 @@
   4.350          val content = #content vs
   4.351      in
   4.352          XML.Elem(("pgip",
   4.353 -                 opt_attr "tag" tag @
   4.354 -                 attr "id" id @
   4.355 -                 opt_attr "destid" destid @
   4.356 -                 attr "class" class @
   4.357 -                 opt_attr "refid" refid @
   4.358 -                 opt_attr_map string_of_int "refseq" refseq @
   4.359 -                 attr "seq" (string_of_int seq)),
   4.360 +                 PgipTypes.opt_attr "tag" tag @
   4.361 +                 PgipTypes.attr "id" id @
   4.362 +                 PgipTypes.opt_attr "destid" destid @
   4.363 +                 PgipTypes.attr "class" class @
   4.364 +                 PgipTypes.opt_attr "refid" refid @
   4.365 +                 PgipTypes.opt_attr_map string_of_int "refseq" refseq @
   4.366 +                 PgipTypes.attr "seq" (string_of_int seq)),
   4.367                   content)
   4.368      end
   4.369  
   4.370 -fun ready (Ready _) = XML.Elem (("ready", []), [])
   4.371 -
   4.372 -
   4.373 -fun output pgipoutput = case pgipoutput of
   4.374 -    Normalresponse _        => normalresponse pgipoutput
   4.375 -  | Errorresponse _         => errorresponse pgipoutput
   4.376 -  | Informfileloaded _      => informfileloaded pgipoutput
   4.377 -  | Informfileoutdated _    => informfileoutdated pgipoutput
   4.378 -  | Informfileretracted _   => informfileretracted pgipoutput
   4.379 -  | Metainforesponse _      => metainforesponse pgipoutput
   4.380 -  | Lexicalstructure _      => lexicalstructure pgipoutput
   4.381 -  | Proverinfo _            => proverinfo pgipoutput
   4.382 -  | Setids _                => setids pgipoutput
   4.383 -  | Setrefs _               => setrefs pgipoutput
   4.384 -  | Addids _                => addids pgipoutput
   4.385 -  | Delids _                => delids pgipoutput
   4.386 -  | Hasprefs _              => hasprefs pgipoutput
   4.387 -  | Prefval _               => prefval pgipoutput
   4.388 -  | Idvalue _               => idvalue pgipoutput
   4.389 -  | Informguise _           => informguise pgipoutput
   4.390 -  | Parseresult _           => parseresult pgipoutput
   4.391 -  | Usespgip _              => usespgip pgipoutput
   4.392 -  | Usespgml _              => usespgml pgipoutput
   4.393 -  | Pgip _                  => pgip pgipoutput
   4.394 -  | Ready _                 => ready pgipoutput
   4.395 -
   4.396  end
   4.397  
     5.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Mon May 13 20:35:04 2013 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,114 +0,0 @@
     5.4 -(*  Title:      Pure/ProofGeneral/pgip_parser.ML
     5.5 -    Author:     David Aspinall and Makarius
     5.6 -
     5.7 -Parsing theory sources without execution (via keyword classification).
     5.8 -*)
     5.9 -
    5.10 -signature PGIP_PARSER =
    5.11 -sig
    5.12 -  val pgip_parser: Position.T -> string -> PgipMarkup.pgipdocument
    5.13 -end
    5.14 -
    5.15 -structure PgipParser: PGIP_PARSER =
    5.16 -struct
    5.17 -
    5.18 -structure D = PgipMarkup;
    5.19 -structure I = PgipIsabelle;
    5.20 -
    5.21 -
    5.22 -fun badcmd text = [D.Badcmd {text = text}];
    5.23 -
    5.24 -fun thy_begin text =
    5.25 -  (case try (Thy_Header.read Position.none) text of
    5.26 -    NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
    5.27 -  | SOME {name = (name, _), imports, ...} =>
    5.28 -       D.Opentheory {thyname = SOME name, parentnames = map #1 imports, text = text})
    5.29 -  :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
    5.30 -
    5.31 -fun thy_heading text =
    5.32 -  [D.Closeblock {},
    5.33 -   D.Doccomment {text = text},
    5.34 -   D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
    5.35 -
    5.36 -fun thy_decl text =
    5.37 -  [D.Theoryitem {name = NONE, objtype = SOME I.ObjTheoryDecl, text = text}];
    5.38 -
    5.39 -fun goal text =
    5.40 -  [D.Opengoal {thmname = NONE, text = text},
    5.41 -   D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
    5.42 -
    5.43 -fun prf_block text =
    5.44 -  [D.Closeblock {},
    5.45 -   D.Proofstep {text = text},
    5.46 -   D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
    5.47 -
    5.48 -fun prf_open text =
    5.49 - [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody},
    5.50 -  D.Proofstep {text = text}];
    5.51 -
    5.52 -fun proofstep text = [D.Proofstep {text = text}];
    5.53 -fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
    5.54 -
    5.55 -
    5.56 -fun command k f = Symtab.update_new (Keyword.kind_of k, f);
    5.57 -
    5.58 -val command_keywords = Symtab.empty
    5.59 -  |> command Keyword.control          badcmd
    5.60 -  |> command Keyword.diag             (fn text => [D.Spuriouscmd {text = text}])
    5.61 -  |> command Keyword.thy_begin        thy_begin
    5.62 -  |> command Keyword.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
    5.63 -  |> command Keyword.thy_heading1     thy_heading
    5.64 -  |> command Keyword.thy_heading2     thy_heading
    5.65 -  |> command Keyword.thy_heading3     thy_heading
    5.66 -  |> command Keyword.thy_heading4     thy_heading
    5.67 -  |> command Keyword.thy_load         thy_decl
    5.68 -  |> command Keyword.thy_decl         thy_decl
    5.69 -  |> command Keyword.thy_script       thy_decl
    5.70 -  |> command Keyword.thy_goal         goal
    5.71 -  |> command Keyword.qed              closegoal
    5.72 -  |> command Keyword.qed_block        closegoal
    5.73 -  |> command Keyword.qed_global       (fn text => [D.Giveupgoal {text = text}])
    5.74 -  |> command Keyword.prf_heading2     (fn text => [D.Doccomment {text = text}])
    5.75 -  |> command Keyword.prf_heading3     (fn text => [D.Doccomment {text = text}])
    5.76 -  |> command Keyword.prf_heading4     (fn text => [D.Doccomment {text = text}])
    5.77 -  |> command Keyword.prf_goal         goal
    5.78 -  |> command Keyword.prf_block        prf_block
    5.79 -  |> command Keyword.prf_open         prf_open
    5.80 -  |> command Keyword.prf_close        (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
    5.81 -  |> command Keyword.prf_chain        proofstep
    5.82 -  |> command Keyword.prf_decl         proofstep
    5.83 -  |> command Keyword.prf_asm          proofstep
    5.84 -  |> command Keyword.prf_asm_goal     goal
    5.85 -  |> command Keyword.prf_script       proofstep;
    5.86 -
    5.87 -val _ = subset (op =) (map Keyword.kind_of Keyword.kinds, Symtab.keys command_keywords)
    5.88 -  orelse raise Fail "Incomplete coverage of command keywords";
    5.89 -
    5.90 -fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
    5.91 -  | parse_command name text =
    5.92 -      (case Keyword.command_keyword name of
    5.93 -        NONE => [D.Unparseable {text = text}]
    5.94 -      | SOME k =>
    5.95 -          (case Symtab.lookup command_keywords (Keyword.kind_of k) of
    5.96 -            NONE => [D.Unparseable {text = text}]
    5.97 -          | SOME f => f text));
    5.98 -
    5.99 -fun parse_span span =
   5.100 -  let
   5.101 -    val kind = Thy_Syntax.span_kind span;
   5.102 -    val toks = Thy_Syntax.span_content span;
   5.103 -    val text = implode (map (Print_Mode.setmp [] Thy_Syntax.present_token) toks);
   5.104 -  in
   5.105 -    (case kind of
   5.106 -      Thy_Syntax.Command (name, _) => parse_command name text
   5.107 -    | Thy_Syntax.Ignored => [D.Whitespace {text = text}]
   5.108 -    | Thy_Syntax.Malformed => [D.Unparseable {text = text}])
   5.109 -  end;
   5.110 -
   5.111 -
   5.112 -fun pgip_parser pos str =
   5.113 -  Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) pos str
   5.114 -  |> Thy_Syntax.parse_spans
   5.115 -  |> maps parse_span;
   5.116 -
   5.117 -end;
     6.1 --- a/src/Pure/ProofGeneral/pgml.ML	Mon May 13 20:35:04 2013 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,160 +0,0 @@
     6.4 -(*  Title:      Pure/ProofGeneral/pgml.ML
     6.5 -    Author:     David Aspinall
     6.6 -
     6.7 -PGIP abstraction: PGML
     6.8 -*)
     6.9 -
    6.10 -signature PGML =
    6.11 -sig
    6.12 -    type pgmlsym = { name: string, content: string }
    6.13 -
    6.14 -    datatype pgmlatom = Sym of pgmlsym | Str of string
    6.15 -
    6.16 -    datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
    6.17 -
    6.18 -    datatype pgmlplace = Subscript | Superscript | Above | Below
    6.19 -
    6.20 -    datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
    6.21 -
    6.22 -    datatype pgmlaction = Toggle | Button | Menu
    6.23 -
    6.24 -    datatype pgmlterm =
    6.25 -             Atoms of { kind: string option, content: pgmlatom list }
    6.26 -           | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
    6.27 -           | Break of { mandatory: bool option, indent: int option }
    6.28 -           | Subterm of { kind: string option,
    6.29 -                          param: string option,
    6.30 -                          place: pgmlplace option,
    6.31 -                          name: string option,
    6.32 -                          decoration: pgmldec option,
    6.33 -                          action: pgmlaction option,
    6.34 -                          pos: string option,
    6.35 -                          xref: PgipTypes.pgipurl option,
    6.36 -                          content: pgmlterm list }
    6.37 -           | Alt of { kind: string option, content: pgmlterm list }
    6.38 -           | Embed of XML.tree list
    6.39 -           | Raw of XML.tree
    6.40 -
    6.41 -    datatype pgml =
    6.42 -             Pgml of { version: string option, systemid: string option,
    6.43 -                       area: PgipTypes.displayarea option,
    6.44 -                       content: pgmlterm list }
    6.45 -
    6.46 -    val atom_to_xml : pgmlatom -> XML.tree
    6.47 -    val pgmlterm_to_xml : pgmlterm -> XML.tree
    6.48 -
    6.49 -    val pgml_to_xml : pgml -> XML.tree
    6.50 -end
    6.51 -
    6.52 -
    6.53 -structure Pgml : PGML =
    6.54 -struct
    6.55 -    open PgipTypes
    6.56 -
    6.57 -    type pgmlsym = { name: string, content: string }
    6.58 -
    6.59 -    datatype pgmlatom = Sym of pgmlsym | Str of string
    6.60 -
    6.61 -    datatype pgmlorient = HOVOrient | HOrient | VOrient | HVOrient
    6.62 -
    6.63 -    datatype pgmlplace = Subscript | Superscript | Above | Below
    6.64 -
    6.65 -    datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
    6.66 -
    6.67 -    datatype pgmlaction = Toggle | Button | Menu
    6.68 -
    6.69 -    datatype pgmlterm =
    6.70 -             Atoms of { kind: string option, content: pgmlatom list }
    6.71 -           | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
    6.72 -           | Break of { mandatory: bool option, indent: int option }
    6.73 -           | Subterm of { kind: string option,
    6.74 -                          param: string option,
    6.75 -                          place: pgmlplace option,
    6.76 -                          name: string option,
    6.77 -                          decoration: pgmldec option,
    6.78 -                          action: pgmlaction option,
    6.79 -                          pos: string option,
    6.80 -                          xref: PgipTypes.pgipurl option,
    6.81 -                          content: pgmlterm list }
    6.82 -           | Alt of { kind: string option, content: pgmlterm list }
    6.83 -           | Embed of XML.tree list
    6.84 -           | Raw of XML.tree
    6.85 -
    6.86 -
    6.87 -    datatype pgml =
    6.88 -             Pgml of { version: string option, systemid: string option,
    6.89 -                       area: PgipTypes.displayarea option,
    6.90 -                       content: pgmlterm list }
    6.91 -
    6.92 -    fun pgmlorient_to_string HOVOrient = "hov"
    6.93 -      | pgmlorient_to_string HOrient = "h"
    6.94 -      | pgmlorient_to_string VOrient = "v"
    6.95 -      | pgmlorient_to_string HVOrient = "hv"
    6.96 -
    6.97 -    fun pgmlplace_to_string Subscript = "sub"
    6.98 -      | pgmlplace_to_string Superscript = "sup"
    6.99 -      | pgmlplace_to_string Above = "above"
   6.100 -      | pgmlplace_to_string Below = "below"
   6.101 -
   6.102 -    fun pgmldec_to_string Bold = "bold"
   6.103 -      | pgmldec_to_string Italic = "italic"
   6.104 -      | pgmldec_to_string Error = "error"
   6.105 -      | pgmldec_to_string Warning = "warning"
   6.106 -      | pgmldec_to_string Info = "info"
   6.107 -      | pgmldec_to_string (Other s) = "other"
   6.108 -
   6.109 -    fun pgmlaction_to_string Toggle = "toggle"
   6.110 -      | pgmlaction_to_string Button = "button"
   6.111 -      | pgmlaction_to_string Menu = "menu"
   6.112 -
   6.113 -    (* NOTE: we assume strings are already XML escaped here, for convenience in Isabelle;
   6.114 -       would be better not to *)  (* FIXME !??? *)
   6.115 -    fun atom_to_xml (Sym {name, content}) = XML.Elem (("sym", attr "name" name), [XML.Text content])
   6.116 -      | atom_to_xml (Str content) = XML.Text content;
   6.117 -
   6.118 -    fun pgmlterm_to_xml (Atoms {kind, content}) =
   6.119 -        XML.Elem(("atom", opt_attr "kind" kind), map atom_to_xml content)
   6.120 -
   6.121 -      | pgmlterm_to_xml (Box {orient, indent, content}) =
   6.122 -        XML.Elem(("box",
   6.123 -                 opt_attr_map pgmlorient_to_string "orient" orient @
   6.124 -                 opt_attr_map int_to_pgstring "indent" indent),
   6.125 -                 map pgmlterm_to_xml content)
   6.126 -
   6.127 -      | pgmlterm_to_xml (Break {mandatory, indent}) =
   6.128 -        XML.Elem(("break",
   6.129 -                 opt_attr_map bool_to_pgstring "mandatory" mandatory @
   6.130 -                 opt_attr_map int_to_pgstring "indent" indent), [])
   6.131 -
   6.132 -      | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
   6.133 -        XML.Elem(("subterm",
   6.134 -                 opt_attr "kind" kind @
   6.135 -                 opt_attr "param" param @
   6.136 -                 opt_attr_map pgmlplace_to_string "place" place @
   6.137 -                 opt_attr "name" name @
   6.138 -                 opt_attr_map pgmldec_to_string "decoration" decoration @
   6.139 -                 opt_attr_map pgmlaction_to_string "action" action @
   6.140 -                 opt_attr "pos" pos @
   6.141 -                 opt_attr_map string_of_pgipurl "xref" xref),
   6.142 -                 map pgmlterm_to_xml content)
   6.143 -
   6.144 -      | pgmlterm_to_xml (Alt {kind, content}) =
   6.145 -        XML.Elem(("alt", opt_attr "kind" kind), map pgmlterm_to_xml content)
   6.146 -
   6.147 -      | pgmlterm_to_xml (Embed xmls) = XML.Elem(("embed", []), xmls)
   6.148 -
   6.149 -      | pgmlterm_to_xml (Raw xml) = xml
   6.150 -
   6.151 -
   6.152 -    datatype pgml =
   6.153 -             Pgml of { version: string option, systemid: string option,
   6.154 -                       area: PgipTypes.displayarea option,
   6.155 -                       content: pgmlterm list }
   6.156 -
   6.157 -    fun pgml_to_xml (Pgml {version,systemid,area,content}) =
   6.158 -        XML.Elem(("pgml",
   6.159 -                 opt_attr "version" version @
   6.160 -                 opt_attr "systemid" systemid @
   6.161 -                 the_default [] (Option.map PgipTypes.attrs_of_displayarea area)),
   6.162 -                 map pgmlterm_to_xml content)
   6.163 -end
     7.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 20:35:04 2013 +0200
     7.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 21:03:30 2013 +0200
     7.3 @@ -17,12 +17,6 @@
     7.4  structure ProofGeneralPgip : PROOF_GENERAL_PGIP =
     7.5  struct
     7.6  
     7.7 -open PgipTypes;
     7.8 -open PgipMarkup;
     7.9 -open PgipInput;
    7.10 -open PgipOutput;
    7.11 -
    7.12 -
    7.13  (** print mode **)
    7.14  
    7.15  val proof_general_emacsN = "ProofGeneralEmacs";
    7.16 @@ -41,7 +35,7 @@
    7.17    fun pgip_serial () = Unsynchronized.inc pgip_seq
    7.18  
    7.19    fun assemble_pgips pgips =
    7.20 -    Pgip { tag = SOME pgip_tag,
    7.21 +    PgipOutput.Pgip { tag = SOME pgip_tag,
    7.22             class = pgip_class,
    7.23             seq = pgip_serial (),
    7.24             id = pgip_id,
    7.25 @@ -110,7 +104,7 @@
    7.26  
    7.27  local
    7.28  
    7.29 -fun invalid_pgip () = raise PGIP "Invalid PGIP packet received";
    7.30 +fun invalid_pgip () = raise PgipTypes.PGIP "Invalid PGIP packet received";
    7.31  
    7.32  fun output_emacs pgips = Output.urgent_message (output_pgips pgips);
    7.33  
    7.34 @@ -120,7 +114,8 @@
    7.35            {name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype};
    7.36        in
    7.37          ! preferences |> List.app (fn (prefcat, prefs) =>
    7.38 -            output_emacs [Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}])
    7.39 +            output_emacs
    7.40 +              [PgipOutput.Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}])
    7.41        end
    7.42    | process_element_emacs (XML.Elem (("setpref", attrs), data)) =
    7.43        let
    7.44 @@ -157,7 +152,7 @@
    7.45             else ()
    7.46           end
    7.47      | _ => invalid_pgip ())
    7.48 -  end handle PGIP msg => error (msg ^ "\n" ^ str);
    7.49 +  end handle PgipTypes.PGIP msg => error (msg ^ "\n" ^ str);
    7.50  
    7.51  val _ =
    7.52    Outer_Syntax.improper_command
     8.1 --- a/src/Pure/ROOT	Mon May 13 20:35:04 2013 +0200
     8.2 +++ b/src/Pure/ROOT	Mon May 13 21:03:30 2013 +0200
     8.3 @@ -160,13 +160,8 @@
     8.4      "Proof/proof_rewrite_rules.ML"
     8.5      "Proof/proof_syntax.ML"
     8.6      "Proof/reconstruct.ML"
     8.7 -    "ProofGeneral/pgip_input.ML"
     8.8 -    "ProofGeneral/pgip_isabelle.ML"
     8.9 -    "ProofGeneral/pgip_markup.ML"
    8.10      "ProofGeneral/pgip_output.ML"
    8.11 -    "ProofGeneral/pgip_parser.ML"
    8.12      "ProofGeneral/pgip_types.ML"
    8.13 -    "ProofGeneral/pgml.ML"
    8.14      "ProofGeneral/preferences.ML"
    8.15      "ProofGeneral/proof_general_emacs.ML"
    8.16      "ProofGeneral/proof_general_pgip.ML"
     9.1 --- a/src/Pure/ROOT.ML	Mon May 13 20:35:04 2013 +0200
     9.2 +++ b/src/Pure/ROOT.ML	Mon May 13 21:03:30 2013 +0200
     9.3 @@ -299,20 +299,13 @@
     9.4  (* configuration for Proof General *)
     9.5  
     9.6  use "ProofGeneral/pgip_types.ML";
     9.7 -use "ProofGeneral/pgml.ML";
     9.8 -use "ProofGeneral/pgip_markup.ML";
     9.9 -use "ProofGeneral/pgip_input.ML";
    9.10  use "ProofGeneral/pgip_output.ML";
    9.11  
    9.12 -use "ProofGeneral/pgip_isabelle.ML";
    9.13 -
    9.14  (use
    9.15    |> Unsynchronized.setmp Proofterm.proofs 0
    9.16    |> Unsynchronized.setmp Multithreading.max_threads 0)
    9.17    "ProofGeneral/preferences.ML";
    9.18  
    9.19 -use "ProofGeneral/pgip_parser.ML";
    9.20 -
    9.21  use "ProofGeneral/proof_general_pgip.ML";
    9.22  use "ProofGeneral/proof_general_emacs.ML";
    9.23