Add abstraction for objtypes and documents.
authoraspinall
Sun Dec 17 22:43:50 2006 +0100 (2006-12-17)
changeset 218678750fbc28d5c
parent 21866 d589f6f5da65
child 21868 54293c8ea022
Add abstraction for objtypes and documents.
src/Pure/ProofGeneral/README
src/Pure/ProofGeneral/ROOT.ML
src/Pure/ProofGeneral/parsing.ML
src/Pure/ProofGeneral/pgip_input.ML
src/Pure/ProofGeneral/pgip_markup.ML
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/pgip_tests.ML
src/Pure/ProofGeneral/pgip_types.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/README	Sat Dec 16 20:27:56 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/README	Sun Dec 17 22:43:50 2006 +0100
     1.3 @@ -31,6 +31,7 @@
     1.4  For the full PGIP schema and an explanation of it, see:
     1.5  
     1.6     http://proofgeneral.inf.ed.ac.uk/kit
     1.7 +   http://proofgeneral.inf.ed.ac.uk/wiki/Main/PGIP
     1.8  
     1.9  David Aspinall, Dec. 2006.
    1.10  $Id$
     2.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Sat Dec 16 20:27:56 2006 +0100
     2.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Sun Dec 17 22:43:50 2006 +0100
     2.3 @@ -3,11 +3,16 @@
     2.4  use "pgip_input.ML";
     2.5  use "pgip_output.ML";
     2.6  use "pgip.ML";
     2.7 -use "pgip_tests.ML";
     2.8  
     2.9  use "pgip_isabelle.ML";
    2.10  use "preferences.ML";
    2.11  use "parsing.ML";
    2.12  
    2.13 +use "pgip_tests.ML";
    2.14 +
    2.15  (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_pgip.ML";
    2.16  (use |> setmp proofs 1 |> setmp quick_and_dirty true) "proof_general_emacs.ML";
    2.17 +
    2.18 +(* desirable to have tests on UI connection:
    2.19 +  use "pgip_isabelle_tests.ML"
    2.20 +*)
     3.1 --- a/src/Pure/ProofGeneral/parsing.ML	Sat Dec 16 20:27:56 2006 +0100
     3.2 +++ b/src/Pure/ProofGeneral/parsing.ML	Sun Dec 17 22:43:50 2006 +0100
     3.3 @@ -2,12 +2,12 @@
     3.4      ID:         $Id$
     3.5      Author:     David Aspinall
     3.6  
     3.7 -Parsing theory files to add PGIP markup.
     3.8 +Parsing Isabelle theory files to add PGIP markup.
     3.9  *)
    3.10  
    3.11  signature PGIP_PARSER =
    3.12  sig
    3.13 -    val xmls_of_str: string -> XML.content
    3.14 +    val pgip_parser: PgipMarkup.pgip_parser
    3.15  end
    3.16  
    3.17  structure PgipParser : PGIP_PARSER =
    3.18 @@ -18,6 +18,8 @@
    3.19  
    3.20  structure P = OuterParse;
    3.21  
    3.22 +structure D = PgipMarkup;
    3.23 +
    3.24  (* Notes.
    3.25     This is quite tricky, because 1) we need to put back whitespace which
    3.26     was removed during parsing so we can provide markup around commands;
    3.27 @@ -27,7 +29,7 @@
    3.28     Markus June '04) helps do this, but the mechanism is still a bad mess.
    3.29  
    3.30     If we had proper parse trees it would be easy, although having a
    3.31 -   fixed type of trees might be tricky with Isar's extensible parser.
    3.32 +   fixed type of trees might be hard with Isar's extensible parser.
    3.33  
    3.34     Probably the best solution is to produce the meta-information at
    3.35     the same time as the parse, for each command, e.g. by recording a
    3.36 @@ -53,31 +55,17 @@
    3.37  *)
    3.38  
    3.39  local
    3.40 -    fun markup_text str elt = [XML.Elem(elt, [], [XML.Text str])]
    3.41 -    fun markup_text_attrs str elt attrs = [XML.Elem(elt, attrs, [XML.Text str])]
    3.42 -    fun empty elt = [XML.Elem(elt, [], [])]
    3.43  
    3.44 -    fun whitespace str = XML.Elem("whitespace", [], [XML.Text str])
    3.45 +    fun whitespace str = D.Whitespace { text=str }
    3.46  
    3.47      (* an extra token is needed to terminate the command *)
    3.48      val sync = OuterSyntax.scan "\\<^sync>";
    3.49  
    3.50 -    fun named_item_elt_with nameattr toks str elt nameP objtyp =
    3.51 -        let
    3.52 -            val name = (fst (nameP (toks@sync)))
    3.53 -                        handle _ => (error ("Error occurred in name parser for " ^ elt ^
    3.54 -                                            "(objtype: " ^ objtyp ^ ")");
    3.55 -                                     "")
    3.56 -
    3.57 -        in
    3.58 -            [XML.Elem(elt,
    3.59 -                     ((if name="" then [] else [(nameattr, name)])@
    3.60 -                      (if objtyp="" then [] else [("objtype", objtyp)])),
    3.61 -                     [XML.Text str])]
    3.62 -        end
    3.63 -
    3.64 -    val named_item_elt = named_item_elt_with "name"
    3.65 -    val thmnamed_item_elt = named_item_elt_with "thmname"
    3.66 +    fun nameparse elt objtyp nameP toks = 
    3.67 +        (fst (nameP (toks@sync)))
    3.68 +        handle _ => (error ("Error occurred in name parser for " ^ elt ^
    3.69 +                            "(objtype: " ^ objtyp ^ ")");
    3.70 +                     "")
    3.71  
    3.72      fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
    3.73  
    3.74 @@ -100,10 +88,9 @@
    3.75          let
    3.76              val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
    3.77          in
    3.78 -            markup_text_attrs str "opentheory"
    3.79 -                              ([("thyname",thyname)] @
    3.80 -                               (if imports=[] then [] else
    3.81 -                                [("parentnames", (space_implode ";" imports) ^ ";")]))
    3.82 +            [D.Opentheory { thyname=thyname, 
    3.83 +			    parentnames = imports,
    3.84 +			    text = str }]
    3.85          end
    3.86  
    3.87      fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
    3.88 @@ -125,9 +112,12 @@
    3.89                   "oracle",
    3.90                   "declare"]
    3.91  
    3.92 -            val plain_item   = markup_text str "theoryitem"
    3.93 -            val comment_item = markup_text str "doccomment"
    3.94 -            val named_item   = named_item_elt toks str "theoryitem"
    3.95 +            fun named_item nameP ty = 
    3.96 +		[D.Theoryitem {text=str,name=SOME (nameparse "theoryitem" ty nameP toks),objtype=SOME ty}]
    3.97 +	    val plain_item = 
    3.98 +		[D.Theoryitem {text=str,name=NONE,objtype=NONE}]
    3.99 +	    val doccomment = 
   3.100 +		[D.Doccomment {text=str}]
   3.101  
   3.102              val opt_overloaded = P.opt_keyword "overloaded";
   3.103  
   3.104 @@ -147,8 +137,8 @@
   3.105  
   3.106              if member (op =) plain_items name then plain_item
   3.107              else case name of
   3.108 -                     "text"      => comment_item
   3.109 -                   | "text_raw"  => comment_item
   3.110 +                     "text"      => doccomment
   3.111 +                   | "text_raw"  => doccomment
   3.112                     | "typedecl"  => named_item (P.type_args |-- P.name) "type"
   3.113                     | "types"     => named_item (P.type_args |-- P.name) "type"
   3.114                     | "classes"   => named_item P.name "class"
   3.115 @@ -161,7 +151,8 @@
   3.116                     | "lemmas"    => named_item thmnameP "thmset"
   3.117                     | "oracle"    => named_item P.name "oracle"
   3.118                     | "locale"    => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
   3.119 -                   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
   3.120 +                   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); 
   3.121 +			   plain_item)
   3.122          end
   3.123  
   3.124      fun xmls_of_thy_goal (name,toks,str) =
   3.125 @@ -178,60 +169,65 @@
   3.126                                                           fst a) (* a : (bstring * Args.src list) *)
   3.127  
   3.128              val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
   3.129 -            (* TODO: add preference values for attributes
   3.130 -               val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
   3.131 -            *)
   3.132 +	    val thmname = nameparse "opengoal" "theorem" nameP toks
   3.133          in
   3.134 -            (thmnamed_item_elt toks str "opengoal" nameP "") @
   3.135 -            (empty "openblock")
   3.136 +            [D.Opengoal {thmname=SOME thmname, text=str},
   3.137 +             D.Openblock {metavarid=NONE,name=NONE,objtype=SOME "theorem-proof"}]
   3.138          end
   3.139  
   3.140 -    fun xmls_of_qed (name,markup) =
   3.141 +    fun xmls_of_qed (name,str) =
   3.142          let val qedmarkup  =
   3.143                  (case name of
   3.144 -                     "sorry" => markup "postponegoal"
   3.145 -                   | "oops"  => markup "giveupgoal"
   3.146 -                   | "done"  => markup "closegoal"
   3.147 -                   | "by"    => markup "closegoal"  (* nested or toplevel *)
   3.148 -                   | "qed"   => markup "closegoal"  (* nested or toplevel *)
   3.149 -                   | "."     => markup "closegoal"  (* nested or toplevel *)
   3.150 -                   | ".."    => markup "closegoal"  (* nested or toplevel *)
   3.151 +                     "sorry" => D.Postponegoal {text=str}
   3.152 +                   | "oops"  => D.Giveupgoal {text=str}
   3.153 +                   | "done"  => D.Closegoal {text=str}
   3.154 +                   | "by"    => D.Closegoal {text=str}  (* nested or toplevel *)
   3.155 +                   | "qed"   => D.Closegoal {text=str}  (* nested or toplevel *)
   3.156 +                   | "."     => D.Closegoal {text=str}  (* nested or toplevel *)
   3.157 +                   | ".."    => D.Closegoal {text=str}  (* nested or toplevel *)
   3.158                     | other => (* default to closegoal: may be wrong for extns *)
   3.159                                    (parse_warning
   3.160                                         ("Unrecognized qed command: " ^ quote other);
   3.161 -                                       markup "closegoal"))
   3.162 -        in qedmarkup @ (empty "closeblock") end
   3.163 +                                       D.Closegoal {text=str}))
   3.164 +        in qedmarkup :: [D.Closeblock {}] end
   3.165  
   3.166      fun xmls_of_kind kind (name,toks,str) =
   3.167 -    let val markup = markup_text str in
   3.168      case kind of
   3.169 -      "control"        => markup "badcmd"
   3.170 -    | "diag"           => markup "spuriouscmd"
   3.171 +      "control"        => [D.Badcmd {text=str}]
   3.172 +    | "diag"           => [D.Theoryitem {name=NONE,objtype=NONE,
   3.173 +					 text=str}] (* FIXME: check NOT spuriouscmd *)
   3.174      (* theory/files *)
   3.175      | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
   3.176      | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
   3.177 -    | "theory-heading" => markup "doccomment"
   3.178 -    | "theory-script"  => markup "theorystep"
   3.179 -    | "theory-end"     => markup "closetheory"
   3.180 +    | "theory-heading" => [D.Doccomment {text=str}]
   3.181 +    | "theory-script"  => [D.Theoryitem {name=NONE,objtype=NONE,text=str}]
   3.182 +    | "theory-end"     => [D.Closetheory {text=str}]
   3.183      (* proof control *)
   3.184      | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
   3.185 -    | "proof-heading"  => markup "doccomment"
   3.186 -    | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
   3.187 -    | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
   3.188 -    | "proof-open"     => (empty "openblock") @ (markup "proofstep")
   3.189 -    | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
   3.190 -    | "proof-script"   => markup "proofstep"
   3.191 -    | "proof-chain"    => markup "proofstep"
   3.192 -    | "proof-decl"     => markup "proofstep"
   3.193 -    | "proof-asm"      => markup "proofstep"
   3.194 -    | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock")  (* nested proof: obtain *)
   3.195 -    | "qed"            => xmls_of_qed (name,markup)
   3.196 -    | "qed-block"      => xmls_of_qed (name,markup)
   3.197 -    | "qed-global"     => xmls_of_qed (name,markup)
   3.198 -    | other => (* default for anything else is "spuriouscmd", ignored for undo *)
   3.199 +    | "proof-heading"  => [D.Doccomment {text=str}]
   3.200 +
   3.201 +    | "proof-goal"     => (* nested proof: have, show, ... *)
   3.202 +      [D.Opengoal {text=str,thmname=NONE}, 
   3.203 +       D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}]
   3.204 +			  
   3.205 +    | "proof-block"    => [D.Proofstep {text=str}]
   3.206 +    | "proof-open"     => [D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}, 
   3.207 +			   D.Proofstep {text=str} ]
   3.208 +    | "proof-close"    => [D.Proofstep {text=str}, D.Closeblock {}]
   3.209 +    | "proof-script"   => [D.Proofstep {text=str}]
   3.210 +    | "proof-chain"    => [D.Proofstep {text=str}]
   3.211 +    | "proof-decl"     => [D.Proofstep {text=str}]
   3.212 +    | "proof-asm"      => [D.Proofstep {text=str}]
   3.213 +    | "proof-asm-goal" => (* nested proof: obtain, ... *)
   3.214 +      [D.Opengoal {text=str,thmname=NONE}, 
   3.215 +       D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}]
   3.216 +
   3.217 +    | "qed"            => xmls_of_qed (name,str)
   3.218 +    | "qed-block"      => xmls_of_qed (name,str)
   3.219 +    | "qed-global"     => xmls_of_qed (name,str)
   3.220 +    | other => (* default for anything else is "spuriouscmd", ***ignored for undo*** *)
   3.221        (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
   3.222 -       markup "spuriouscmd")
   3.223 -    end
   3.224 +       [D.Spuriouscmd {text=str}])
   3.225  in
   3.226  
   3.227  fun xmls_of_transition (name,str,toks) =
   3.228 @@ -241,22 +237,19 @@
   3.229            SOME k => (xmls_of_kind k (name,toks,str))
   3.230          | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
   3.231            (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
   3.232 -           markup_text str "spuriouscmd")
   3.233 +           [D.Spuriouscmd {text=str}])
   3.234     end
   3.235  
   3.236 -fun markup_toks [] _ = []
   3.237 -  | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x
   3.238 -
   3.239  fun markup_comment_whs [] = []
   3.240    | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
   3.241      let
   3.242          val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
   3.243      in
   3.244          if (prewhs <> []) then
   3.245 -            whitespace (implode (map OuterLex.unparse prewhs))
   3.246 +            D.Whitespace {text=implode (map OuterLex.unparse prewhs)}
   3.247              :: (markup_comment_whs rest)
   3.248          else
   3.249 -            (markup_text (OuterLex.unparse t) "comment") @
   3.250 +            D.Comment {text=OuterLex.unparse t} ::
   3.251              (markup_comment_whs ts)
   3.252      end
   3.253  
   3.254 @@ -277,22 +270,26 @@
   3.255      in
   3.256          ((markup_comment_whs prewhs) @
   3.257           (if (length rest2 = length rest1)  then []
   3.258 -          else markup_text (implode
   3.259 -                                (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
   3.260 -               "doccomment") @
   3.261 -         (markup_comment_whs postwhs),
   3.262 -         Library.take (length rest3 - 1,rest3))
   3.263 +          else 
   3.264 +	      [D.Doccomment 
   3.265 +		   {text= implode
   3.266 +                          (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1)))}]
   3.267 +              @
   3.268 +              (markup_comment_whs postwhs)),
   3.269 +              Library.take (length rest3 - 1,rest3))
   3.270      end
   3.271  
   3.272  fun xmls_of_impropers toks =
   3.273      let
   3.274          val (xmls,rest) = xmls_pre_cmd toks
   3.275 +	val unparsed =  
   3.276 +	    case rest of [] => []
   3.277 +		       | _ => [D.Unparseable 
   3.278 +			      {text= implode (map OuterLex.unparse rest)}]
   3.279      in
   3.280 -        xmls @ (markup_toks rest "unparseable")
   3.281 +        xmls @ unparsed
   3.282      end
   3.283  
   3.284 -fun markup_unparseable str = markup_text str "unparseable"
   3.285 -
   3.286  end
   3.287  
   3.288  
   3.289 @@ -307,7 +304,7 @@
   3.290          else match_tokens (t::ts,ws,w::vs)
   3.291        | match_tokens _ = error ("match_tokens: mismatched input parse")
   3.292  in
   3.293 -    fun xmls_of_str str =
   3.294 +    fun pgip_parser str =
   3.295      let
   3.296         (* parsing:   See outer_syntax.ML/toplevel_source *)
   3.297         fun parse_loop ([],[],xmls) = xmls
   3.298 @@ -332,7 +329,7 @@
   3.299           in
   3.300               parse_loop (OuterSyntax.read toks, toks, [])
   3.301           end)
   3.302 -           handle _ => markup_unparseable str
   3.303 +           handle _ => [D.Unparseable {text=str}]
   3.304      end
   3.305  end
   3.306  
     4.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Sat Dec 16 20:27:56 2006 +0100
     4.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Sun Dec 17 22:43:50 2006 +0100
     4.3 @@ -29,11 +29,15 @@
     4.4      | Redostep       of { }
     4.5      | Abortgoal      of { }
     4.6      | Forget         of { thyname: string option, name: string option, 
     4.7 -                          objtype: string option }
     4.8 +                          objtype: PgipTypes.objtype option }
     4.9      | Restoregoal    of { thmname : string }
    4.10      (* context inspection commands *)
    4.11 -    | Askids         of { thyname:string option, objtype:string option }
    4.12 -    | Showid         of { thyname:string option, objtype:string, name:string }
    4.13 +    | Askids         of { url: PgipTypes.pgipurl option,
    4.14 +			  thyname: PgipTypes.objname option,
    4.15 +			  objtype: PgipTypes.objtype option }
    4.16 +    | Showid         of { thyname: PgipTypes.objname option, 
    4.17 +			  objtype: PgipTypes.objtype, 
    4.18 +			  name: PgipTypes.objname }
    4.19      | Askguise       of { }
    4.20      | Parsescript    of { text: string, location: PgipTypes.location,
    4.21                            systemdata: string option } 
    4.22 @@ -89,11 +93,15 @@
    4.23         | Redostep	of { }
    4.24         | Abortgoal	of { }
    4.25         | Forget		of { thyname: string option, name: string option, 
    4.26 -			     objtype: string option }
    4.27 +			     objtype: PgipTypes.objtype option }
    4.28         | Restoregoal    of { thmname : string }
    4.29         (* context inspection commands *)
    4.30 -       | Askids		of { thyname:string option, objtype:string option }
    4.31 -       | Showid		of { thyname:string option, objtype:string, name:string }
    4.32 +       | Askids         of { url: PgipTypes.pgipurl option,
    4.33 +			     thyname: PgipTypes.objname option,
    4.34 +			     objtype: PgipTypes.objtype option }
    4.35 +       | Showid         of { thyname: PgipTypes.objname option, 
    4.36 +			     objtype: PgipTypes.objtype, 
    4.37 +			     name: PgipTypes.objname }
    4.38         | Askguise	of { }
    4.39         | Parsescript	of { text: string, location: location,
    4.40  			     systemdata: string option } 
    4.41 @@ -123,12 +131,18 @@
    4.42  
    4.43      val thyname_attro = get_attr_opt "thyname"
    4.44      val thyname_attr = get_attr "thyname"
    4.45 -    val objtype_attro = get_attr_opt "objtype"
    4.46 -    val objtype_attr = get_attr "objtype"
    4.47      val name_attr = get_attr "name"
    4.48      val name_attro = get_attr_opt "name"
    4.49      val thmname_attr = get_attr "thmname"
    4.50  
    4.51 +    fun objtype_attro attrs = if has_attr "objtype" attrs then
    4.52 +				  SOME (objtype_of_attrs attrs)
    4.53 +			      else NONE
    4.54 +
    4.55 +    fun pgipurl_attro attrs = if has_attr "url" attrs then
    4.56 +				  SOME (pgipurl_of_attrs attrs)
    4.57 +			      else NONE
    4.58 +
    4.59      val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
    4.60      val prefcat_attr = get_attr_opt "prefcategory"
    4.61  
    4.62 @@ -173,10 +187,11 @@
    4.63  				  objtype = objtype_attro attrs }
    4.64     | "restoregoal"    => Restoregoal { thmname = thmname_attr attrs}
    4.65     (* proofctxt: improper commands *)
    4.66 -   | "askids"         => Askids { thyname = thyname_attro attrs, 
    4.67 +   | "askids"         => Askids { url = pgipurl_attro attrs,
    4.68 +				  thyname = thyname_attro attrs, 
    4.69  				  objtype = objtype_attro attrs }
    4.70     | "showid"         => Showid { thyname = thyname_attro attrs,
    4.71 -				  objtype = objtype_attr attrs,
    4.72 +				  objtype = objtype_of_attrs attrs,
    4.73  				  name = name_attr attrs }
    4.74     | "askguise"       => Askguise { }
    4.75     | "parsescript"    => Parsescript { text = (xmltext data),
     5.1 --- a/src/Pure/ProofGeneral/pgip_markup.ML	Sat Dec 16 20:27:56 2006 +0100
     5.2 +++ b/src/Pure/ProofGeneral/pgip_markup.ML	Sun Dec 17 22:43:50 2006 +0100
     5.3 @@ -9,9 +9,9 @@
     5.4  sig
     5.5    (* Generic markup on sequential, non-overlapping pieces of proof text *)
     5.6    datatype pgipdoc = 
     5.7 -    Openblock     of { metavarid: string option }
     5.8 +    Openblock     of { metavarid: string option, name: string option, objtype: string option }
     5.9    | Closeblock    of { }
    5.10 -  | Opentheory    of { thyname: string option, parentnames: string list , text: string}
    5.11 +  | Opentheory    of { thyname: string, parentnames: string list , text: string}
    5.12    | Theoryitem    of { name: string option, objtype: string option, text: string }
    5.13    | Closetheory   of { text: string }
    5.14    | Opengoal	  of { thmname: string option, text: string }
    5.15 @@ -24,6 +24,7 @@
    5.16    | Whitespace    of { text: string }
    5.17    | Spuriouscmd   of { text: string }
    5.18    | Badcmd        of { text: string }
    5.19 +  | Unparseable	  of { text: string } 
    5.20    | Metainfo 	  of { name: string option, text: string }
    5.21    (* Last three for PGIP literate markup only: *)
    5.22    | Litcomment	  of { format: string option, content: XML.content }
    5.23 @@ -43,10 +44,11 @@
    5.24  struct
    5.25     open PgipTypes
    5.26  
    5.27 +(* PGIP 3 idea: replace opentheory, opengoal, etc. by just openblock with corresponding objtype? *)
    5.28    datatype pgipdoc = 
    5.29 -    Openblock     of { metavarid: string option }
    5.30 +    Openblock     of { metavarid: string option, name: string option, objtype: string option }
    5.31    | Closeblock    of { }
    5.32 -  | Opentheory    of { thyname: string option, parentnames: string list , text: string}
    5.33 +  | Opentheory    of { thyname: string, parentnames: string list, text: string}
    5.34    | Theoryitem    of { name: string option, objtype: string option, text: string }
    5.35    | Closetheory   of { text: string }
    5.36    | Opengoal	  of { thmname: string option, text: string }
    5.37 @@ -59,6 +61,7 @@
    5.38    | Whitespace    of { text: string }
    5.39    | Spuriouscmd   of { text: string }
    5.40    | Badcmd        of { text: string }
    5.41 +  | Unparseable	  of { text: string }
    5.42    | Metainfo 	  of { name: string option, text: string }
    5.43    | Litcomment	  of { format: string option, content: XML.content }
    5.44    | Showcode	  of { show: bool }				 
    5.45 @@ -76,6 +79,15 @@
    5.46  	 | Closeblock vs => 
    5.47  	   XML.Elem("closeblock", [], [])
    5.48  	   
    5.49 +	 | Opentheory vs  => 
    5.50 +	   XML.Elem("opentheory", 
    5.51 +		    attr "thyname" (#thyname vs) @
    5.52 +		    opt_attr "parentnames"
    5.53 +			     (case (#parentnames vs) 
    5.54 +			       of [] => NONE
    5.55 +				| ps => SOME (space_implode ";" ps)),
    5.56 +		    [XML.Text (#text vs)])
    5.57 +
    5.58  	 | Theoryitem vs => 
    5.59  	   XML.Elem("theoryitem", 
    5.60  		    opt_attr "name" (#name vs) @
    5.61 @@ -105,6 +117,9 @@
    5.62  	 | Comment vs => 
    5.63  	   XML.Elem("comment", [], [XML.Text (#text vs)])
    5.64  
    5.65 +	 | Whitespace vs => 
    5.66 +	   XML.Elem("whitespace", [], [XML.Text (#text vs)])
    5.67 +
    5.68  	 | Doccomment vs => 
    5.69  	   XML.Elem("doccomment", [], [XML.Text (#text vs)])
    5.70  
    5.71 @@ -114,6 +129,9 @@
    5.72  	 | Badcmd vs => 
    5.73  	   XML.Elem("badcmd", [], [XML.Text (#text vs)])
    5.74  
    5.75 +	 | Unparseable vs => 
    5.76 +	   XML.Elem("unparseable", [], [XML.Text (#text vs)])
    5.77 +
    5.78  	 | Metainfo vs => 
    5.79  	   XML.Elem("metainfo", opt_attr "name" (#name vs), 
    5.80  		    [XML.Text (#text vs)])
    5.81 @@ -148,6 +166,7 @@
    5.82       | Whitespace vs => #text vs
    5.83       | Spuriouscmd vs => #text vs
    5.84       | Badcmd vs => #text vs
    5.85 +     | Unparseable vs => #text vs
    5.86       | Metainfo vs => #text vs
    5.87       | _ => ""
    5.88  
     6.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Sat Dec 16 20:27:56 2006 +0100
     6.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Sun Dec 17 22:43:50 2006 +0100
     6.3 @@ -30,21 +30,21 @@
     6.4                                 descr: string, 
     6.5                                 url: Url.T, 
     6.6                                 filenameextns: string }
     6.7 -    | Idtable             of { objtype: string, 
     6.8 -                               context: string option, 
     6.9 -                               ids: string list }
    6.10 -    | Setids              of { idtables: XML.content }
    6.11 -    | Delids              of { idtables: XML.content }
    6.12 -    | Addids              of { idtables: XML.content }
    6.13 +    | Setids              of { idtables: PgipTypes.idtable list  }
    6.14 +    | Delids              of { idtables: PgipTypes.idtable list }
    6.15 +    | Addids              of { idtables: PgipTypes.idtable list }
    6.16      | Hasprefs            of { prefcategory: string option, 
    6.17                                 prefs: PgipTypes.preference list }
    6.18      | Prefval             of { name: string, value: string }
    6.19 -    | Idvalue             of { name: string, objtype: string, text: XML.content }
    6.20 +    | Idvalue             of { name: PgipTypes.objname, 
    6.21 +			       objtype: PgipTypes.objtype, 
    6.22 +			       text: XML.content }
    6.23      | Informguise         of { file : PgipTypes.pgipurl option,  
    6.24 -                               theory: string option, 
    6.25 -                               theorem: string option, 
    6.26 +                               theory: PgipTypes.objname option, 
    6.27 +                               theorem: PgipTypes.objname option, 
    6.28                                 proofpos: int option }
    6.29 -    | Parseresult         of { attrs: XML.attributes, content: XML.content }
    6.30 +    | Parseresult         of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument, 
    6.31 +			       errs: XML.content } (* errs to become PGML *)
    6.32      | Usespgip            of { version: string, 
    6.33                                 pgipelems: (string * bool * string list) list }
    6.34      | Usespgml            of { version: string }
    6.35 @@ -77,16 +77,20 @@
    6.36         | Lexicalstructure    of { content: XML.content }
    6.37         | Proverinfo          of { name: string, version: string, instance: string,
    6.38                                    descr: string, url: Url.T, filenameextns: string }
    6.39 -       | Idtable             of { objtype: string, context: string option, ids: string list }
    6.40 -       | Setids              of { idtables: XML.content }
    6.41 -       | Delids              of { idtables: XML.content }
    6.42 -       | Addids              of { idtables: XML.content }
    6.43 +       | Setids              of { idtables: PgipTypes.idtable list  }
    6.44 +       | Delids              of { idtables: PgipTypes.idtable list }
    6.45 +       | Addids              of { idtables: PgipTypes.idtable list }
    6.46         | Hasprefs            of { prefcategory: string option, prefs: preference list }
    6.47         | Prefval             of { name: string, value: string }
    6.48 -       | Idvalue             of { name: string, objtype: string, text: XML.content }
    6.49 -       | Informguise         of { file : pgipurl option,  theory: string option, 
    6.50 -                                  theorem: string option, proofpos: int option }
    6.51 -       | Parseresult         of { attrs: XML.attributes, content: XML.content }
    6.52 +       | Idvalue             of { name: PgipTypes.objname, 
    6.53 +				  objtype: PgipTypes.objtype, 
    6.54 +				  text: XML.content }
    6.55 +       | Informguise         of { file : PgipTypes.pgipurl option,  
    6.56 +				  theory: PgipTypes.objname option, 
    6.57 +				  theorem: PgipTypes.objname option, 
    6.58 +				  proofpos: int option }
    6.59 +       | Parseresult         of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
    6.60 +				  errs: XML.content } (* errs to become PGML *)
    6.61         | Usespgip            of { version: string, 
    6.62                                    pgipelems: (string * bool * string list) list }
    6.63         | Usespgml            of { version: string }
    6.64 @@ -189,39 +193,25 @@
    6.65                   [])
    6.66      end
    6.67  
    6.68 -fun idtable vs = 
    6.69 -    let 
    6.70 -        val objtype = #objtype vs
    6.71 -        val objtype_attrs = attr "objtype" objtype
    6.72 -        val context = #context vs
    6.73 -        val context_attrs = opt_attr "context" context
    6.74 -        val ids = #ids vs
    6.75 -        val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
    6.76 -    in 
    6.77 -        XML.Elem ("idtable",
    6.78 -                  objtype_attrs @ context_attrs,
    6.79 -                  ids_content)
    6.80 -    end
    6.81 -
    6.82  fun setids vs =
    6.83      let
    6.84          val idtables = #idtables vs
    6.85      in
    6.86 -        XML.Elem ("setids",[],idtables)
    6.87 +        XML.Elem ("setids",[],map idtable_to_xml idtables)
    6.88      end
    6.89  
    6.90  fun addids vs =
    6.91      let
    6.92          val idtables = #idtables vs
    6.93      in
    6.94 -        XML.Elem ("addids",[],idtables)
    6.95 +        XML.Elem ("addids",[],map idtable_to_xml idtables)
    6.96      end
    6.97  
    6.98  fun delids vs =
    6.99      let
   6.100          val idtables = #idtables vs
   6.101      in
   6.102 -        XML.Elem ("delids",[],idtables)
   6.103 +        XML.Elem ("delids",[],map idtable_to_xml idtables)
   6.104      end
   6.105  
   6.106  
   6.107 @@ -258,10 +248,10 @@
   6.108  fun idvalue vs =
   6.109      let 
   6.110          val name = #name vs
   6.111 -        val objtype = #objtype vs
   6.112 +	val objtype_attrs = attrs_of_objtype (#objtype vs)
   6.113          val text = #text vs
   6.114      in
   6.115 -        XML.Elem("idvalue", [("name",name),("objtype",objtype)], text)
   6.116 +        XML.Elem("idvalue", attr "name" name @ objtype_attrs, text)
   6.117      end 
   6.118  
   6.119  
   6.120 @@ -286,9 +276,11 @@
   6.121  fun parseresult vs =
   6.122      let
   6.123          val attrs = #attrs vs
   6.124 -        val content = #content vs
   6.125 +        val doc = #doc vs
   6.126 +        val errs = #errs vs
   6.127 +	val xmldoc = PgipMarkup.output_doc doc
   6.128      in 
   6.129 -        XML.Elem("parseresult", attrs, content)
   6.130 +        XML.Elem("parseresult", attrs, errs@xmldoc)
   6.131      end
   6.132  
   6.133  fun usespgip vs =
   6.134 @@ -341,7 +333,6 @@
   6.135   | Metainforesponse vs     => metainforesponse vs
   6.136   | Lexicalstructure vs     => lexicalstructure vs
   6.137   | Proverinfo vs           => proverinfo vs
   6.138 - | Idtable vs              => idtable vs
   6.139   | Setids vs               => setids vs
   6.140   | Addids vs               => addids vs
   6.141   | Delids vs               => delids vs
     7.1 --- a/src/Pure/ProofGeneral/pgip_tests.ML	Sat Dec 16 20:27:56 2006 +0100
     7.2 +++ b/src/Pure/ProofGeneral/pgip_tests.ML	Sun Dec 17 22:43:50 2006 +0100
     7.3 @@ -82,6 +82,14 @@
     7.4  
     7.5  end
     7.6  
     7.7 +(** pgip_markup.ML **)
     7.8 +local
     7.9 +open PgipMarkup
    7.10 +in
    7.11 +val _ = ()
    7.12 +end
    7.13 +
    7.14 +
    7.15  (** pgip_output.ML **)
    7.16  local
    7.17  open PgipOutput
    7.18 @@ -89,3 +97,25 @@
    7.19  val _ = ()
    7.20  end
    7.21  
    7.22 +
    7.23 +(** parsing.ML **)
    7.24 +local
    7.25 +open PgipMarkup
    7.26 +open PgipParser
    7.27 +fun asseqp a b =
    7.28 +    if (pgip_parser a)=b then ()
    7.29 +    else error("PGIP test: expected two parses to be equal, for input:\n" ^ a)
    7.30 +
    7.31 +in
    7.32 +val _ = 
    7.33 +    asseqp "theory A imports Bthy Cthy Dthy begin"
    7.34 +    [Opentheory
    7.35 +         {text = "theory A imports Bthy Cthy Dthy begin",
    7.36 +          thyname = "A",
    7.37 +          parentnames = ["Bthy", "Cthy", "Dthy"]}];
    7.38 +
    7.39 +val _ = 
    7.40 +    asseqp "end" 
    7.41 +   [Closetheory {text = "end"}];
    7.42 +
    7.43 +end
     8.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Sat Dec 16 20:27:56 2006 +0100
     8.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Sun Dec 17 22:43:50 2006 +0100
     8.3 @@ -5,9 +5,22 @@
     8.4  PGIP abstraction: types and conversions
     8.5  *)
     8.6  
     8.7 -(* TODO: add objtypes and PGML *)
     8.8 +(* TODO: PGML *)
     8.9  signature PGIPTYPES =
    8.10  sig
    8.11 +    (* Object types: the types of values which can be manipulated externally.
    8.12 +       Ideally a list of other types would be configured as a parameter. *)
    8.13 +    datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment  
    8.14 +		     | ObjTerm | ObjType | ObjOther of string
    8.15 +  
    8.16 +    (* Names for values of objtypes (i.e. prover identifiers). Could be a parameter.
    8.17 +       Names for ObjFiles are URIs. *)
    8.18 +    type objname = string
    8.19 +
    8.20 +    type idtable = { context: objname option,    (* container's objname *)
    8.21 +                     objtype: objtype, 
    8.22 +                     ids: objname list }
    8.23 +
    8.24      (* Types and values (used for preferences and dialogs) *)
    8.25  
    8.26      datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat
    8.27 @@ -50,6 +63,12 @@
    8.28  signature PGIPTYPES_OPNS = 
    8.29  sig
    8.30      include PGIPTYPES
    8.31 + 
    8.32 +    (* Object types *)
    8.33 +    val name_of_objtype  : objtype -> string
    8.34 +    val attrs_of_objtype : objtype -> XML.attributes
    8.35 +    val objtype_of_attrs : XML.attributes -> objtype		        (* raises PGIP *)
    8.36 +    val idtable_to_xml   : idtable -> XML.tree
    8.37  
    8.38      (* Values as XML strings *)
    8.39      val read_pgipint	   : (int option * int option) -> string -> int (* raises PGIP *)
    8.40 @@ -76,10 +95,12 @@
    8.41      val pgipurl_of_url : Url.T -> pgipurl	       (* raises PGIP *)
    8.42      val pgipurl_of_string : string -> pgipurl	       (* raises PGIP *)
    8.43      val pgipurl_of_path : Path.T -> pgipurl
    8.44 +    val path_of_pgipurl : pgipurl -> Path.T
    8.45      val attrs_of_pgipurl : pgipurl -> XML.attributes
    8.46      val pgipurl_of_attrs : XML.attributes -> pgipurl   (* raises PGIP *)
    8.47  
    8.48      (* XML utils, only for PGIP code *)
    8.49 +    val has_attr       : string -> XML.attributes -> bool
    8.50      val attr	       : string -> string -> XML.attributes
    8.51      val opt_attr       : string -> string option -> XML.attributes
    8.52      val opt_attr_map   : ('a -> string) -> string -> 'a option -> XML.attributes
    8.53 @@ -92,7 +113,9 @@
    8.54  struct
    8.55  exception PGIP of string
    8.56  
    8.57 -(** Utils **)
    8.58 +(** XML utils **)
    8.59 +
    8.60 +fun has_attr attr attrs = AList.defined (op =) attrs attr
    8.61  
    8.62  fun get_attr_opt attr attrs = AList.lookup (op =) attrs attr
    8.63  
    8.64 @@ -113,6 +136,50 @@
    8.65  
    8.66  val opt_attr = opt_attr_map I
    8.67  
    8.68 +
    8.69 +(** Objtypes **)
    8.70 +
    8.71 +datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment  
    8.72 +		 | ObjTerm | ObjType | ObjOther of string
    8.73 +
    8.74 +fun name_of_objtype obj = 
    8.75 +    case obj of 
    8.76 +	ObjFile    => "file"
    8.77 +      | ObjTheory  => "theory"
    8.78 +      | ObjTheorem => "theorem"
    8.79 +      | ObjComment => "comment"
    8.80 +      | ObjTerm    => "term"
    8.81 +      | ObjType    => "type"
    8.82 +      | ObjOther s => s
    8.83 +
    8.84 +val attrs_of_objtype = (attr "objtype") o name_of_objtype
    8.85 +
    8.86 +fun objtype_of_attrs attrs = case get_attr "objtype" attrs of
    8.87 +       "file" => ObjFile
    8.88 +     | "theory" => ObjTheory
    8.89 +     | "theorem" => ObjTheorem
    8.90 +     | "comment" => ObjComment
    8.91 +     | "term" => ObjTerm
    8.92 +     | "type" => ObjType
    8.93 +     | s => ObjOther s    (* where s mem other_objtypes_parameter *)
    8.94 +
    8.95 +type objname = string
    8.96 +type idtable = { context: objname option,    (* container's objname *)
    8.97 +                 objtype: objtype, 
    8.98 +                 ids: objname list }
    8.99 +
   8.100 +fun idtable_to_xml {context, objtype, ids} = 
   8.101 +    let 
   8.102 +        val objtype_attrs = attrs_of_objtype objtype
   8.103 +        val context_attrs = opt_attr "context" context
   8.104 +        val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids
   8.105 +    in 
   8.106 +        XML.Elem ("idtable",
   8.107 +                  objtype_attrs @ context_attrs,
   8.108 +                  ids_content)
   8.109 +    end
   8.110 +
   8.111 +
   8.112  (** Types and values **)
   8.113  
   8.114  (* readers and writers for values represented in XML strings *)
   8.115 @@ -258,9 +325,7 @@
   8.116    | pgval_to_string (_,(Pgvalstring s)) = string_to_pgstring s
   8.117  
   8.118  
   8.119 -(** URLs: only local files **)
   8.120 -
   8.121 -type pgipurl = Path.T
   8.122 +type pgipurl = Path.T    (* URLs: only local files *)
   8.123  
   8.124  datatype displayarea = Status | Message | Display | Other of string
   8.125  
   8.126 @@ -278,6 +343,7 @@
   8.127  
   8.128  (** Url operations **)
   8.129  
   8.130 +
   8.131  fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
   8.132  	case Url.explode url of
   8.133              (Url.File path) => path
   8.134 @@ -285,6 +351,8 @@
   8.135  		       
   8.136  fun pgipurl_of_path p = p
   8.137  
   8.138 +fun path_of_pgipurl p = p  (* potentially raises PGIP *)
   8.139 +
   8.140  fun attrs_of_pgipurl purl = 
   8.141      [("url", "file:" ^ (XML.text (File.platform_path (File.full_path purl))))]
   8.142  
     9.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Dec 16 20:27:56 2006 +0100
     9.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Dec 17 22:43:50 2006 +0100
     9.3 @@ -294,7 +294,6 @@
     9.4  
     9.5  val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
     9.6  val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
     9.7 -val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
     9.8  
     9.9  fun proper_inform_file_processed file state =
    9.10    let val name = thy_name file in
    9.11 @@ -414,37 +413,6 @@
    9.12  end
    9.13  
    9.14  
    9.15 -(* PGIP identifier tables (prover objects). [incomplete] *)
    9.16 -
    9.17 -local
    9.18 -    (* TODO: objtypes should be in pgip_types.ML *)
    9.19 -    val objtype_thy  = "theory"
    9.20 -    val objtype_thm  = "theorem"
    9.21 -    val objtype_term = "term"
    9.22 -    val objtype_type = "type"
    9.23 -
    9.24 -    fun xml_idtable ty ctx ids =
    9.25 -        PgipOutput.output (Idtable {objtype=ty,context=ctx,ids=ids})
    9.26 -in
    9.27 -
    9.28 -fun setids t = issue_pgip (Setids {idtables = [t]})
    9.29 -fun addids t = issue_pgip (Addids {idtables = [t]})
    9.30 -fun delids t = issue_pgip (Delids {idtables = [t]})
    9.31 -
    9.32 -fun delallids ty = setids (xml_idtable ty NONE [])
    9.33 -
    9.34 -fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
    9.35 -fun clear_thy_idtable () = delallids objtype_thy
    9.36 -
    9.37 -fun send_thm_idtable ctx thy =
    9.38 -    addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
    9.39 -
    9.40 -fun clear_thm_idtable () = delallids objtype_thm
    9.41 -
    9.42 -(* fun send_type_idtable thy = TODO, it's a bit low-level messy
    9.43 -   & maybe not so useful anyway *)
    9.44 -
    9.45 -end
    9.46  
    9.47  
    9.48  (* Sending commands to Isar *)
    9.49 @@ -469,7 +437,7 @@
    9.50      end
    9.51  
    9.52  
    9.53 -(**** PGIP actions ****)
    9.54 +(******* PGIP actions *******)
    9.55  
    9.56  
    9.57  (* Responses to each of the PGIP input commands. 
    9.58 @@ -558,21 +526,45 @@
    9.59  fun abortgoal vs = isarcmd "ProofGeneral.kill_proof" 
    9.60  
    9.61  
    9.62 +(*** PGIP identifier tables ***)
    9.63 +
    9.64 +fun setids t = issue_pgip (Setids {idtables = [t]})
    9.65 +fun addids t = issue_pgip (Addids {idtables = [t]})
    9.66 +fun delids t = issue_pgip (Delids {idtables = [t]})
    9.67 +
    9.68 +(*
    9.69 + fun delallids ty = 
    9.70 +     issue_pgip (Setids {idtables = 
    9.71 +	 		[{context=NONE,objtype=ty,ids=[]}]}) *)
    9.72 +
    9.73  fun askids vs = 
    9.74      let
    9.75 -	val thyname = #thyname vs
    9.76 -	val objtype = #objtype vs
    9.77 +	val url = #url vs	     (* ask for identifiers within a file *)
    9.78 +	val thyname = #thyname vs    (* ask for identifiers within a theory *)
    9.79 +	val objtype = #objtype vs    (* ask for identifiers of a particular type *)
    9.80 +
    9.81 +	fun idtable ty ctx ids = {objtype=ty,context=ctx,ids=ids}
    9.82 +
    9.83 +	val thms_of_thy = (map fst) o PureThy.thms_of o ThyInfo.get_theory
    9.84      in 
    9.85 +(*	case (url_attr,thyname,objtype) of
    9.86 +	    (NONE,NONE,NONE) => 
    9.87 +*)	    (* top-level: return *)
    9.88 +
    9.89  	(* TODO: add askids for "file" here, which returns single theory with same name *)
    9.90 +        (* FIXME: objtypes on both sides *)
    9.91  	case (thyname,objtype) of 
    9.92 -           (* only theories known in top context *)
    9.93 -	   (NONE, NONE) =>  send_thy_idtable NONE (ThyInfo.names())
    9.94 -	 | (NONE, SOME "theory")  => send_thy_idtable NONE (ThyInfo.names())
    9.95 -	 | (SOME thy, SOME "theory") => send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
    9.96 -	 | (SOME thy, SOME "theorem") => send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
    9.97 -	 | (SOME thy, NONE) => (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
    9.98 -                               send_thm_idtable (SOME thy) (ThyInfo.get_theory thy))
    9.99 -	 | (_, SOME ot) => error ("No objects of type "^(quote ot)^" are available here.")
   9.100 +           (* only files known in top context *)
   9.101 +	   (NONE, NONE)		      => setids (idtable ObjFile NONE (ThyInfo.names())) (*FIXME: uris?*)
   9.102 +	 | (NONE, SOME ObjFile)        => setids (idtable ObjFile NONE (ThyInfo.names())) (* ditto *)
   9.103 +	 | (SOME fi, SOME ObjFile)     => setids (idtable ObjTheory (SOME fi) [fi]) (* FIXME: lookup file *)
   9.104 +	 | (NONE, SOME ObjTheory)      => setids (idtable ObjTheory NONE (ThyInfo.names()))
   9.105 +	 | (SOME thy, SOME ObjTheory)  => setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy))
   9.106 +	 | (SOME thy, SOME ObjTheorem) => setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy))
   9.107 +         (* next case is both of above.  FIXME: cleanup this *)					 
   9.108 +	 | (SOME thy, NONE) => (setids (idtable ObjTheory (SOME thy) (ThyInfo.get_preds thy));
   9.109 +				setids (idtable ObjTheorem (SOME thy) (thms_of_thy thy)))
   9.110 +	 | (_, SOME ot) => error ("No objects of type "^(PgipTypes.name_of_objtype ot)^" are available here.")
   9.111      end
   9.112  
   9.113  local
   9.114 @@ -590,7 +582,7 @@
   9.115      let
   9.116  	val thyname = #thyname vs
   9.117  	val objtype = #objtype vs
   9.118 -	val name = #objtype vs
   9.119 +	val name = #name vs
   9.120  	val topthy = Toplevel.theory_of o Toplevel.get_state
   9.121  
   9.122  	fun idvalue objtype name strings =
   9.123 @@ -600,18 +592,20 @@
   9.124  	fun pthm thy name = print_thm (get_thm thy (Name name))
   9.125      in 
   9.126  	case (thyname, objtype) of 
   9.127 -	    (_,"theory") =>
   9.128 -	    with_displaywrap (idvalue "theory" name) 
   9.129 +	    (_,ObjTheory) =>
   9.130 +	    with_displaywrap (idvalue ObjTheory name) 
   9.131  			     (fn ()=>(print_theory (ThyInfo.get_theory name)))
   9.132 -	  | (SOME thy, "theorem") =>
   9.133 -	    with_displaywrap (idvalue "theorem" name) 
   9.134 +	  | (SOME thy, ObjTheorem) =>
   9.135 +	    with_displaywrap (idvalue ObjTheorem name) 
   9.136  			     (fn ()=>(pthm (ThyInfo.get_theory thy) name))
   9.137 -	  | (NONE, "theorem") =>
   9.138 -	    with_displaywrap (idvalue "theorem" name) 
   9.139 +	  | (NONE, ObjTheorem) =>
   9.140 +	    with_displaywrap (idvalue ObjTheorem name) 
   9.141  			     (fn ()=>pthm (topthy()) name)
   9.142 -	  | (_, ot) => error ("Cannot show objects of type "^ot)
   9.143 +	  | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
   9.144      end
   9.145  
   9.146 +(*** Inspecting state ***)
   9.147 +
   9.148  (* The file which is currently being processed interactively.  
   9.149     In the pre-PGIP code, this was informed to Isabelle and the theory loader
   9.150     on completion, but that allows for circularity in case we read
   9.151 @@ -649,15 +643,16 @@
   9.152  	val systemdata = #systemdata vs      
   9.153  	val location = #location vs   (* TODO: extract position *)
   9.154  
   9.155 -        val _ = start_delay_msgs ()  (* gather parsing messages *)
   9.156 -        val xmls = PgipParser.xmls_of_str text
   9.157 +        val _ = start_delay_msgs ()   (* gather parsing errs/warns *)
   9.158 +        val doc = PgipParser.pgip_parser text
   9.159          val errs = end_delayed_msgs ()
   9.160  
   9.161  	val sysattrs = PgipTypes.opt_attr "systemdata" systemdata
   9.162  	val locattrs = PgipTypes.attrs_of_location location
   9.163       in
   9.164          issue_pgip (Parseresult { attrs= sysattrs@locattrs,
   9.165 -				  content = (map PgipOutput.output errs)@xmls })
   9.166 +				  doc = doc,
   9.167 +				  errs = (map PgipOutput.output errs) })
   9.168      end
   9.169  
   9.170  fun showproofstate vs = isarcmd "pr"
   9.171 @@ -685,6 +680,8 @@
   9.172  	isarcmd ("print_" ^ arg)   (* FIXME: isatool doc?.  Return URLs, maybe? *)
   9.173      end
   9.174  
   9.175 +(*** Theory ***)
   9.176 +
   9.177  fun doitem vs =
   9.178      let
   9.179  	val text = #text vs
   9.180 @@ -708,6 +705,61 @@
   9.181  	isarcmd ("kill_thy " ^ quote thyname)
   9.182      end
   9.183  
   9.184 +
   9.185 +(*** Files ***)
   9.186 +
   9.187 +(* Path management: we allow theory files to have dependencies in
   9.188 +   their own directory, but when we change directory for a new file we
   9.189 +   remove the path.  Leaving it there can cause confusion with
   9.190 +   difference in batch mode.
   9.191 +   NB: PGIP does not assume that the prover has a load path. 
   9.192 +*)
   9.193 +
   9.194 +local
   9.195 +    val current_working_dir = ref (NONE : string option)
   9.196 +in
   9.197 +fun changecwd_dir newdirpath = 
   9.198 +   let 
   9.199 +       val newdir = File.platform_path newdirpath
   9.200 +   in 
   9.201 +       (case (!current_working_dir) of
   9.202 +            NONE => ()
   9.203 +          | SOME dir => ThyLoad.del_path dir;
   9.204 +        ThyLoad.add_path newdir;
   9.205 +        current_working_dir := SOME newdir)
   9.206 +   end
   9.207 +end
   9.208 +
   9.209 +fun changecwd vs = 
   9.210 +    let 
   9.211 +	val url = #url vs
   9.212 +	val newdir = PgipTypes.path_of_pgipurl url
   9.213 +    in
   9.214 +	changecwd_dir url
   9.215 +    end
   9.216 +
   9.217 +fun openfile vs =
   9.218 +  let 
   9.219 +      val url = #url vs
   9.220 +      val filepath = PgipTypes.path_of_pgipurl url
   9.221 +      val filedir = Path.dir filepath
   9.222 +      val thy_name = Path.implode o #1 o Path.split_ext o Path.base
   9.223 +      val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
   9.224 +  in
   9.225 +      case !currently_open_file of
   9.226 +          SOME f => raise PGIP ("<openfile> when a file is already open! ")
   9.227 +        | NONE => (openfile_retract filepath;
   9.228 +		   changecwd_dir filedir;
   9.229 +		   currently_open_file := SOME url)
   9.230 +  end
   9.231 +
   9.232 +fun closefile vs =
   9.233 +    case !currently_open_file of
   9.234 +        SOME f => (proper_inform_file_processed (File.platform_path f) 
   9.235 +						(Isar.state());
   9.236 +                   currently_open_file := NONE)
   9.237 +      | NONE => raise PGIP ("<closefile> when no file is open!")
   9.238 +
   9.239  fun loadfile vs = 
   9.240      let 
   9.241  	val url = #url vs
   9.242 @@ -717,23 +769,6 @@
   9.243            | NONE => use_thy_or_ml_file (File.platform_path url)
   9.244      end
   9.245  
   9.246 -fun openfile vs =
   9.247 -  let 
   9.248 -      val url = #url vs
   9.249 -  in
   9.250 -      case !currently_open_file of
   9.251 -          SOME f => raise PGIP ("<openfile> when a file is already open! ")
   9.252 -        | NONE => (openfile_retract (File.platform_path url);
   9.253 -		   currently_open_file := SOME url) (*(File.platform_path url))*)
   9.254 -  end
   9.255 -
   9.256 -fun closefile vs =
   9.257 -    case !currently_open_file of
   9.258 -        SOME f => (proper_inform_file_processed (File.platform_path f) 
   9.259 -						(Isar.state());
   9.260 -                   currently_open_file := NONE)
   9.261 -      | NONE => raise PGIP ("<closefile> when no file is open!")
   9.262 -
   9.263  fun abortfile vs =
   9.264      case !currently_open_file of
   9.265          SOME f => (isarcmd "init_toplevel";
   9.266 @@ -749,29 +784,8 @@
   9.267            | NONE => inform_file_retracted (File.platform_path url)
   9.268      end
   9.269  
   9.270 -(* Path management: we allow theory files to have dependencies in
   9.271 -   their own directory, but when we change directory for a new file we
   9.272 -   remove the path.  Leaving it there can cause confusion with
   9.273 -   difference in batch mode.
   9.274 -   NB: PGIP does not assume that the prover has a load path. 
   9.275 -*)
   9.276  
   9.277 -local
   9.278 -    val current_working_dir = ref (NONE : string option)
   9.279 -in
   9.280 -fun changecwd vs = 
   9.281 -    let 
   9.282 -	val url = #url vs
   9.283 -	val newdir = File.platform_path url
   9.284 -    in
   9.285 -        (case (!current_working_dir) of
   9.286 -             NONE => ()
   9.287 -           | SOME dir => ThyLoad.del_path dir;
   9.288 -         ThyLoad.add_path newdir;
   9.289 -         current_working_dir := SOME newdir)
   9.290 -    end
   9.291 -end
   9.292 -
   9.293 +(*** System ***)
   9.294  
   9.295  fun systemcmd vs =
   9.296    let