get rid of tabs;
authorwenzelm
Wed Aug 27 12:00:28 2008 +0200 (2008-08-27)
changeset 280201ff5167592ba
parent 28019 359764333bf4
child 28021 32acf3c6cd12
get rid of tabs;
src/Pure/Isar/locale.ML
src/Pure/ProofGeneral/pgip_input.ML
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/pgip_tests.ML
src/Pure/ProofGeneral/pgip_types.ML
src/Pure/ProofGeneral/pgml.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Aug 27 11:49:50 2008 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Aug 27 12:00:28 2008 +0200
     1.3 @@ -1595,10 +1595,10 @@
     1.4      val id' = prep_id id
     1.5      val eqns' = case get_reg id'
     1.6        of NONE => eqns
     1.7 -	| SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
     1.8 +        | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
     1.9              handle Termtab.DUP t =>
    1.10 -	      error ("Conflicting interpreting equations for term " ^
    1.11 -		quote (Syntax.string_of_term ctxt t))
    1.12 +              error ("Conflicting interpreting equations for term " ^
    1.13 +                quote (Syntax.string_of_term ctxt t))
    1.14    in ((id', eqns'), eqns') end;
    1.15  
    1.16  
     2.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Wed Aug 27 11:49:50 2008 +0200
     2.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Wed Aug 27 12:00:28 2008 +0200
     2.3 @@ -30,15 +30,15 @@
     2.4      | Restoregoal    of { thmname : string }
     2.5      (* context inspection commands *)
     2.6      | Askids         of { url: PgipTypes.pgipurl option,
     2.7 -			  thyname: PgipTypes.objname option,
     2.8 -			  objtype: PgipTypes.objtype option }
     2.9 +                          thyname: PgipTypes.objname option,
    2.10 +                          objtype: PgipTypes.objtype option }
    2.11      | Askrefs        of { url: PgipTypes.pgipurl option,
    2.12 -			  thyname: PgipTypes.objname option,
    2.13 -			  objtype: PgipTypes.objtype option,
    2.14 -			  name: PgipTypes.objname option }
    2.15 +                          thyname: PgipTypes.objname option,
    2.16 +                          objtype: PgipTypes.objtype option,
    2.17 +                          name: PgipTypes.objname option }
    2.18      | Showid         of { thyname: PgipTypes.objname option, 
    2.19 -			  objtype: PgipTypes.objtype, 
    2.20 -			  name: PgipTypes.objname }
    2.21 +                          objtype: PgipTypes.objtype, 
    2.22 +                          name: PgipTypes.objname }
    2.23      | Askguise       of { }
    2.24      | Parsescript    of { text: string, location: PgipTypes.location,
    2.25                            systemdata: string option } 
    2.26 @@ -74,59 +74,59 @@
    2.27  (*** PGIP input ***)
    2.28  
    2.29  datatype pgipinput = 
    2.30 -	 (* protocol/prover config *)
    2.31 -	 Askpgip 	of { }
    2.32 -       | Askpgml 	of { } 
    2.33 -       | Askconfig	of { }
    2.34 -       | Askprefs	of { }
    2.35 -       | Setpref 	of { name:string, prefcategory:string option, value:string }
    2.36 -       | Getpref 	of { name:string, prefcategory:string option }
    2.37 +         (* protocol/prover config *)
    2.38 +         Askpgip        of { }
    2.39 +       | Askpgml        of { } 
    2.40 +       | Askconfig      of { }
    2.41 +       | Askprefs       of { }
    2.42 +       | Setpref        of { name:string, prefcategory:string option, value:string }
    2.43 +       | Getpref        of { name:string, prefcategory:string option }
    2.44         (* prover control *)
    2.45 -       | Proverinit 	of { }
    2.46 -       | Proverexit 	of { }
    2.47 +       | Proverinit     of { }
    2.48 +       | Proverexit     of { }
    2.49         | Setproverflag  of { flagname:string, value: bool }
    2.50         (* improper proof commands: control proof state *)
    2.51 -       | Dostep		of { text: string }
    2.52 -       | Undostep	of { times: int }
    2.53 -       | Redostep	of { }
    2.54 -       | Abortgoal	of { }
    2.55 -       | Forget		of { thyname: string option, name: string option, 
    2.56 -			     objtype: PgipTypes.objtype option }
    2.57 +       | Dostep         of { text: string }
    2.58 +       | Undostep       of { times: int }
    2.59 +       | Redostep       of { }
    2.60 +       | Abortgoal      of { }
    2.61 +       | Forget         of { thyname: string option, name: string option, 
    2.62 +                             objtype: PgipTypes.objtype option }
    2.63         | Restoregoal    of { thmname : string }
    2.64         (* context inspection commands *)
    2.65         | Askids         of { url: PgipTypes.pgipurl option,
    2.66 -			     thyname: PgipTypes.objname option,
    2.67 -			     objtype: PgipTypes.objtype option }
    2.68 +                             thyname: PgipTypes.objname option,
    2.69 +                             objtype: PgipTypes.objtype option }
    2.70         | Askrefs        of { url: PgipTypes.pgipurl option,
    2.71 -			     thyname: PgipTypes.objname option,
    2.72 -			     objtype: PgipTypes.objtype option,
    2.73 -			     name: PgipTypes.objname option }
    2.74 +                             thyname: PgipTypes.objname option,
    2.75 +                             objtype: PgipTypes.objtype option,
    2.76 +                             name: PgipTypes.objname option }
    2.77         | Showid         of { thyname: PgipTypes.objname option, 
    2.78 -			     objtype: PgipTypes.objtype, 
    2.79 -			     name: PgipTypes.objname }
    2.80 -       | Askguise	of { }
    2.81 -       | Parsescript	of { text: string, location: location,
    2.82 -			     systemdata: string option } 
    2.83 +                             objtype: PgipTypes.objtype, 
    2.84 +                             name: PgipTypes.objname }
    2.85 +       | Askguise       of { }
    2.86 +       | Parsescript    of { text: string, location: location,
    2.87 +                             systemdata: string option } 
    2.88         | Showproofstate of { }
    2.89 -       | Showctxt	of { }
    2.90 +       | Showctxt       of { }
    2.91         | Searchtheorems of { arg: string }
    2.92         | Setlinewidth   of { width: int }
    2.93 -       | Viewdoc	of { arg: string }
    2.94 +       | Viewdoc        of { arg: string }
    2.95         (* improper theory-level commands *)
    2.96 -       | Doitem		of { text: string }
    2.97 -       | Undoitem	of { }
    2.98 -       | Redoitem	of { }
    2.99 -       | Aborttheory	of { }
   2.100 +       | Doitem         of { text: string }
   2.101 +       | Undoitem       of { }
   2.102 +       | Redoitem       of { }
   2.103 +       | Aborttheory    of { }
   2.104         | Retracttheory  of { thyname: string }
   2.105 -       | Loadfile 	of { url: pgipurl }
   2.106 -       | Openfile 	of { url: pgipurl }
   2.107 -       | Closefile	of { }
   2.108 -       | Abortfile	of { }
   2.109 +       | Loadfile       of { url: pgipurl }
   2.110 +       | Openfile       of { url: pgipurl }
   2.111 +       | Closefile      of { }
   2.112 +       | Abortfile      of { }
   2.113         | Retractfile    of { url: pgipurl }
   2.114 -       | Changecwd 	of { url: pgipurl }
   2.115 -       | Systemcmd 	of { arg: string }
   2.116 +       | Changecwd      of { url: pgipurl }
   2.117 +       | Systemcmd      of { arg: string }
   2.118         (* unofficial escape command for debugging *)
   2.119 -       | Quitpgip	of { }
   2.120 +       | Quitpgip       of { }
   2.121  
   2.122  (* Extracting content from input XML elements to make a PGIPinput *)
   2.123  local
   2.124 @@ -140,12 +140,12 @@
   2.125      val value_attr = get_attr "value"
   2.126  
   2.127      fun objtype_attro attrs = if has_attr "objtype" attrs then
   2.128 -				  SOME (objtype_of_attrs attrs)
   2.129 -			      else NONE
   2.130 +                                  SOME (objtype_of_attrs attrs)
   2.131 +                              else NONE
   2.132  
   2.133      fun pgipurl_attro attrs = if has_attr "url" attrs then
   2.134 -				  SOME (pgipurl_of_attrs attrs)
   2.135 -			      else NONE
   2.136 +                                  SOME (pgipurl_of_attrs attrs)
   2.137 +                              else NONE
   2.138  
   2.139      val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
   2.140      val prefcat_attr = get_attr_opt "prefcategory"
   2.141 @@ -171,39 +171,39 @@
   2.142     (* proverconfig *)
   2.143     | "askprefs"       => Askprefs { }
   2.144     | "getpref"        => Getpref { name = name_attr attrs, 
   2.145 -				   prefcategory = prefcat_attr attrs }
   2.146 +                                   prefcategory = prefcat_attr attrs }
   2.147     | "setpref"        => Setpref { name = name_attr attrs, 
   2.148 -				   prefcategory = prefcat_attr attrs,
   2.149 -				   value = xmltext data }
   2.150 +                                   prefcategory = prefcat_attr attrs,
   2.151 +                                   value = xmltext data }
   2.152     (* provercontrol *)
   2.153     | "proverinit"     => Proverinit { }
   2.154     | "proverexit"     => Proverexit { }
   2.155     | "setproverflag"  => Setproverflag { flagname = flagname_attr attrs,
   2.156 -					 value = read_pgipbool (value_attr attrs) }
   2.157 +                                         value = read_pgipbool (value_attr attrs) }
   2.158     (* improperproofcmd: improper commands not in script *)
   2.159     | "dostep"         => Dostep    { text = xmltext data }
   2.160     | "undostep"       => Undostep  { times = times_attr attrs }
   2.161     | "redostep"       => Redostep  { } 
   2.162     | "abortgoal"      => Abortgoal { }
   2.163     | "forget"         => Forget { thyname = thyname_attro attrs, 
   2.164 -				  name = name_attro attrs,
   2.165 -				  objtype = objtype_attro attrs }
   2.166 +                                  name = name_attro attrs,
   2.167 +                                  objtype = objtype_attro attrs }
   2.168     | "restoregoal"    => Restoregoal { thmname = thmname_attr attrs}
   2.169     (* proofctxt: improper commands *)
   2.170     | "askids"         => Askids { url = pgipurl_attro attrs,
   2.171 -				  thyname = thyname_attro attrs, 
   2.172 -				  objtype = objtype_attro attrs }
   2.173 +                                  thyname = thyname_attro attrs, 
   2.174 +                                  objtype = objtype_attro attrs }
   2.175     | "askrefs"        => Askrefs { url = pgipurl_attro attrs,
   2.176 -				   thyname = thyname_attro attrs, 
   2.177 -				   objtype = objtype_attro attrs,
   2.178 -				   name = name_attro attrs }
   2.179 +                                   thyname = thyname_attro attrs, 
   2.180 +                                   objtype = objtype_attro attrs,
   2.181 +                                   name = name_attro attrs }
   2.182     | "showid"         => Showid { thyname = thyname_attro attrs,
   2.183 -				  objtype = objtype_of_attrs attrs,
   2.184 -				  name = name_attr attrs }
   2.185 +                                  objtype = objtype_of_attrs attrs,
   2.186 +                                  name = name_attr attrs }
   2.187     | "askguise"       => Askguise { }
   2.188     | "parsescript"    => Parsescript { text = (xmltext data),
   2.189 -				       systemdata = get_attr_opt "systemdata" attrs,
   2.190 -				       location = location_of_attrs attrs }
   2.191 +                                       systemdata = get_attr_opt "systemdata" attrs,
   2.192 +                                       location = location_of_attrs attrs }
   2.193     | "showproofstate" => Showproofstate { }
   2.194     | "showctxt"       => Showctxt { }
   2.195     | "searchtheorems" => Searchtheorems { arg = xmltext data }
   2.196 @@ -223,17 +223,17 @@
   2.197     | "changecwd"      => Changecwd { url = pgipurl_of_attrs attrs }
   2.198     | "systemcmd"      => Systemcmd { arg = xmltext data }
   2.199     (* unofficial command for debugging *)
   2.200 -   | "quitpgip"	=> Quitpgip { }
   2.201 +   | "quitpgip" => Quitpgip { }
   2.202  
   2.203     (* We allow sending proper document markup too; we map it back to dostep   *)
   2.204     (* and strip out metainfo elements. Markup correctness isn't checked: this *)
   2.205     (* is a compatibility measure to make it easy for interfaces.              *)
   2.206     | x => if (x mem PgipMarkup.doc_markup_elements) then
   2.207 -	      if (x mem PgipMarkup.doc_markup_elements_ignored) then
   2.208 -		  raise NoAction
   2.209 -	      else 
   2.210 -		  Dostep { text = xmltext data } (* could separate out Doitem too *)
   2.211 -	  else raise Unknown) 
   2.212 +              if (x mem PgipMarkup.doc_markup_elements_ignored) then
   2.213 +                  raise NoAction
   2.214 +              else 
   2.215 +                  Dostep { text = xmltext data } (* could separate out Doitem too *)
   2.216 +          else raise Unknown) 
   2.217      handle Unknown => NONE | NoAction => NONE
   2.218  end
   2.219  
     3.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Wed Aug 27 11:49:50 2008 +0200
     3.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Wed Aug 27 12:00:28 2008 +0200
     3.3 @@ -32,21 +32,21 @@
     3.4                                 prefs: PgipTypes.preference list }
     3.5      | Prefval             of { name: string, value: string }
     3.6      | Setrefs             of { url: PgipTypes.pgipurl option,
     3.7 -			       thyname: PgipTypes.objname option,
     3.8 -			       objtype: PgipTypes.objtype option,
     3.9 -			       name: PgipTypes.objname option,
    3.10 -			       idtables: PgipTypes.idtable list,
    3.11 -			       fileurls : PgipTypes.pgipurl list }
    3.12 +                               thyname: PgipTypes.objname option,
    3.13 +                               objtype: PgipTypes.objtype option,
    3.14 +                               name: PgipTypes.objname option,
    3.15 +                               idtables: PgipTypes.idtable list,
    3.16 +                               fileurls : PgipTypes.pgipurl list }
    3.17      | Idvalue             of { thyname: PgipTypes.objname option,
    3.18 -			       objtype: PgipTypes.objtype, 
    3.19 -			       name: PgipTypes.objname, 
    3.20 -			       text: XML.tree list }
    3.21 +                               objtype: PgipTypes.objtype, 
    3.22 +                               name: PgipTypes.objname, 
    3.23 +                               text: XML.tree list }
    3.24      | Informguise         of { file : PgipTypes.pgipurl option,  
    3.25                                 theory: PgipTypes.objname option, 
    3.26                                 theorem: PgipTypes.objname option, 
    3.27                                 proofpos: int option }
    3.28      | Parseresult         of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument, 
    3.29 -			       errs: XML.tree list } (* errs to become PGML *)
    3.30 +                               errs: XML.tree list } (* errs to become PGML *)
    3.31      | Usespgip            of { version: string, 
    3.32                                 pgipelems: (string * bool * string list) list }
    3.33      | Usespgml            of { version: string }
    3.34 @@ -67,10 +67,10 @@
    3.35  open PgipTypes
    3.36  
    3.37  datatype pgipoutput = 
    3.38 -	 Normalresponse      of { content: XML.tree list }
    3.39 +         Normalresponse      of { content: XML.tree list }
    3.40         | Errorresponse       of { fatality: fatality, 
    3.41                                    location: location option, 
    3.42 -				  content: XML.tree list }
    3.43 +                                  content: XML.tree list }
    3.44         | Informfileloaded    of { url: Path.T, completed: bool }
    3.45         | Informfileoutdated  of { url: Path.T, completed: bool }
    3.46         | Informfileretracted of { url: Path.T, completed: bool }
    3.47 @@ -84,21 +84,21 @@
    3.48         | Hasprefs            of { prefcategory: string option, prefs: preference list }
    3.49         | Prefval             of { name: string, value: string }
    3.50         | Idvalue             of { thyname: PgipTypes.objname option,
    3.51 -				  objtype: PgipTypes.objtype, 
    3.52 -				  name: PgipTypes.objname, 
    3.53 -				  text: XML.tree list }
    3.54 +                                  objtype: PgipTypes.objtype, 
    3.55 +                                  name: PgipTypes.objname, 
    3.56 +                                  text: XML.tree list }
    3.57         | Setrefs             of { url: PgipTypes.pgipurl option,
    3.58 -				  thyname: PgipTypes.objname option,
    3.59 -				  objtype: PgipTypes.objtype option,
    3.60 -				  name: PgipTypes.objname option,
    3.61 -				  idtables: PgipTypes.idtable list,
    3.62 -				  fileurls : PgipTypes.pgipurl list }
    3.63 +                                  thyname: PgipTypes.objname option,
    3.64 +                                  objtype: PgipTypes.objtype option,
    3.65 +                                  name: PgipTypes.objname option,
    3.66 +                                  idtables: PgipTypes.idtable list,
    3.67 +                                  fileurls : PgipTypes.pgipurl list }
    3.68         | Informguise         of { file : PgipTypes.pgipurl option,  
    3.69 -				  theory: PgipTypes.objname option, 
    3.70 -				  theorem: PgipTypes.objname option, 
    3.71 -				  proofpos: int option }
    3.72 +                                  theory: PgipTypes.objname option, 
    3.73 +                                  theorem: PgipTypes.objname option, 
    3.74 +                                  proofpos: int option }
    3.75         | Parseresult         of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
    3.76 -				  errs: XML.tree list } (* errs to become PGML *)
    3.77 +                                  errs: XML.tree list } (* errs to become PGML *)
    3.78         | Usespgip            of { version: string, 
    3.79                                    pgipelems: (string * bool * string list) list }
    3.80         | Usespgml            of { version: string }
    3.81 @@ -119,7 +119,7 @@
    3.82          val content = #content vs
    3.83      in
    3.84          XML.Elem ("normalresponse", 
    3.85 -		  [],
    3.86 +                  [],
    3.87                    content)
    3.88      end
    3.89  
    3.90 @@ -141,9 +141,9 @@
    3.91          val completed = #completed vs
    3.92      in
    3.93          XML.Elem ("informfileloaded", 
    3.94 -		  attrs_of_pgipurl url @ 
    3.95 -		  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
    3.96 -		  [])
    3.97 +                  attrs_of_pgipurl url @ 
    3.98 +                  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
    3.99 +                  [])
   3.100      end
   3.101  
   3.102  fun informfileoutdated (Informfileoutdated vs) =
   3.103 @@ -152,9 +152,9 @@
   3.104          val completed = #completed vs
   3.105      in
   3.106          XML.Elem ("informfileoutdated", 
   3.107 -		  attrs_of_pgipurl url @ 
   3.108 -		  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
   3.109 -		  [])
   3.110 +                  attrs_of_pgipurl url @ 
   3.111 +                  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
   3.112 +                  [])
   3.113      end
   3.114  
   3.115  fun informfileretracted (Informfileretracted vs) =
   3.116 @@ -163,9 +163,9 @@
   3.117          val completed = #completed vs
   3.118      in
   3.119          XML.Elem ("informfileretracted", 
   3.120 -		  attrs_of_pgipurl url @ 
   3.121 -		  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
   3.122 -		  [])
   3.123 +                  attrs_of_pgipurl url @ 
   3.124 +                  (attr "completed" (PgipTypes.bool_to_pgstring completed)),
   3.125 +                  [])
   3.126      end
   3.127  
   3.128  fun metainforesponse (Metainforesponse vs) =
   3.129 @@ -211,21 +211,21 @@
   3.130  
   3.131  fun setrefs (Setrefs vs) =
   3.132      let
   3.133 -	val url = #url vs
   3.134 -	val thyname = #thyname vs
   3.135 -	val objtype = #objtype vs
   3.136 -	val name = #name vs
   3.137 +        val url = #url vs
   3.138 +        val thyname = #thyname vs
   3.139 +        val objtype = #objtype vs
   3.140 +        val name = #name vs
   3.141          val idtables = #idtables vs
   3.142          val fileurls = #fileurls vs
   3.143 -	fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
   3.144 +        fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
   3.145      in
   3.146          XML.Elem ("setrefs",
   3.147 -		  (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @ 
   3.148 -		  (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
   3.149 -		  (opt_attr "thyname" thyname) @
   3.150 -		  (opt_attr "name" name),
   3.151 -		  (map idtable_to_xml idtables) @ 
   3.152 -		  (map fileurl_to_xml fileurls))
   3.153 +                  (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @ 
   3.154 +                  (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
   3.155 +                  (opt_attr "thyname" thyname) @
   3.156 +                  (opt_attr "name" name),
   3.157 +                  (map idtable_to_xml idtables) @ 
   3.158 +                  (map fileurl_to_xml fileurls))
   3.159      end
   3.160  
   3.161  fun addids (Addids vs) =
   3.162 @@ -260,16 +260,16 @@
   3.163  
   3.164  fun idvalue (Idvalue vs) =
   3.165      let 
   3.166 -	val objtype_attrs = attrs_of_objtype (#objtype vs)
   3.167 -	val thyname = #thyname vs
   3.168 +        val objtype_attrs = attrs_of_objtype (#objtype vs)
   3.169 +        val thyname = #thyname vs
   3.170          val name = #name vs
   3.171          val text = #text vs
   3.172      in
   3.173          XML.Elem("idvalue", 
   3.174 -		 objtype_attrs @
   3.175 -		 (opt_attr "thyname" thyname) @
   3.176 -		 (attr "name" name),
   3.177 -		 text)
   3.178 +                 objtype_attrs @
   3.179 +                 (opt_attr "thyname" thyname) @
   3.180 +                 (attr "name" name),
   3.181 +                 text)
   3.182      end
   3.183  
   3.184  fun informguise (Informguise vs) =
   3.185 @@ -295,7 +295,7 @@
   3.186          val attrs = #attrs vs
   3.187          val doc = #doc vs
   3.188          val errs = #errs vs
   3.189 -	val xmldoc = PgipMarkup.output_doc doc
   3.190 +        val xmldoc = PgipMarkup.output_doc doc
   3.191      in 
   3.192          XML.Elem("parseresult", attrs, errs @ xmldoc)
   3.193      end
     4.1 --- a/src/Pure/ProofGeneral/pgip_tests.ML	Wed Aug 27 11:49:50 2008 +0200
     4.2 +++ b/src/Pure/ProofGeneral/pgip_tests.ML	Wed Aug 27 12:00:28 2008 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4  fun asseq_p toS a b =
     4.5      if a=b then ()
     4.6      else error("PGIP test: expected these two values to be equal:\n" ^
     4.7 -	       (toS a) ^"\n and: \n" ^ (toS b))
     4.8 +               (toS a) ^"\n and: \n" ^ (toS b))
     4.9  
    4.10  val asseqx = asseq_p XML.string_of
    4.11  val asseqs = asseq_p I
    4.12 @@ -40,18 +40,18 @@
    4.13  
    4.14  local
    4.15      val choices = Pgipchoice [Pgipdtype (NONE,Pgipbool), Pgipdtype (NONE,Pgipnat), 
    4.16 -			      Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
    4.17 +                              Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
    4.18  in
    4.19  val _ = asseqs (pgval_to_string (read_pgval choices "45")) "45";
    4.20  val _ = asseqs (pgval_to_string (read_pgval choices "foo")) "foo";
    4.21  val _ = asseqs (pgval_to_string (read_pgval choices "true")) "true";
    4.22  val _ = asseqs (pgval_to_string (read_pgval choices "")) "";
    4.23  val _ = (asseqs (pgval_to_string (read_pgval choices "-37")) "-37"; 
    4.24 -	 error "pgip_tests: should fail") handle PGIP _ => ()
    4.25 +         error "pgip_tests: should fail") handle PGIP _ => ()
    4.26  end
    4.27  
    4.28  val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
    4.29 -		 default=SOME "true", pgiptype=Pgipbool})
    4.30 +                 default=SOME "true", pgiptype=Pgipbool})
    4.31         (XML.parse "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
    4.32  end
    4.33  
    4.34 @@ -60,8 +60,8 @@
    4.35  local
    4.36  
    4.37  fun e str = case XML.parse str of 
    4.38 -		(XML.Elem args) => args
    4.39 -	      | _ => error("Expected to get an XML Element")
    4.40 +                (XML.Elem args) => args
    4.41 +              | _ => error("Expected to get an XML Element")
    4.42  
    4.43  open PgipInput;
    4.44  open PgipTypes;
    4.45 @@ -83,7 +83,7 @@
    4.46  val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
    4.47  *)
    4.48  val _ = asseqi "<askrefs thyname='foo' objtype='theory'/>" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
    4.49 -									  objtype=SOME ObjTheory,name=NONE}));
    4.50 +                                                                          objtype=SOME ObjTheory,name=NONE}));
    4.51  val _ = asseqi "<otherelt/>" NONE;
    4.52  
    4.53  end
     5.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Wed Aug 27 11:49:50 2008 +0200
     5.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Wed Aug 27 12:00:28 2008 +0200
     5.3 @@ -11,7 +11,7 @@
     5.4      (* Object types: the types of values which can be manipulated externally.
     5.5         Ideally a list of other types would be configured as a parameter. *)
     5.6      datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment  
     5.7 -		     | ObjTerm | ObjType | ObjOther of string
     5.8 +                     | ObjTerm | ObjType | ObjOther of string
     5.9    
    5.10      (* Names for values of objtypes (i.e. prover identifiers). Could be a parameter.
    5.11         Names for ObjFiles are URIs. *)
    5.12 @@ -24,7 +24,7 @@
    5.13      (* Types and values (used for preferences and dialogs) *)
    5.14  
    5.15      datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat
    5.16 -		      | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
    5.17 +                      | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
    5.18  
    5.19      and pgipdtype = Pgipdtype of string option * pgiptype  (* type with opt. description *)
    5.20  
    5.21 @@ -44,17 +44,17 @@
    5.22  
    5.23      (* File location *)
    5.24      type location = { descr: string option,
    5.25 -		      url: pgipurl option,
    5.26 -		      line: int option,
    5.27 -		      column: int option,
    5.28 -		      char: int option,
    5.29 -		      length: int option }
    5.30 +                      url: pgipurl option,
    5.31 +                      line: int option,
    5.32 +                      column: int option,
    5.33 +                      char: int option,
    5.34 +                      length: int option }
    5.35  
    5.36      (* Prover preference *)   
    5.37      type preference = { name: string,
    5.38 -			descr: string option,
    5.39 -			default: string option,
    5.40 -			pgiptype: pgiptype }
    5.41 +                        descr: string option,
    5.42 +                        default: string option,
    5.43 +                        pgiptype: pgiptype }
    5.44  end
    5.45  
    5.46  signature PGIPTYPES_OPNS = 
    5.47 @@ -64,21 +64,21 @@
    5.48      (* Object types *)
    5.49      val name_of_objtype  : objtype -> string
    5.50      val attrs_of_objtype : objtype -> XML.attributes
    5.51 -    val objtype_of_attrs : XML.attributes -> objtype		        (* raises PGIP *)
    5.52 +    val objtype_of_attrs : XML.attributes -> objtype                    (* raises PGIP *)
    5.53      val idtable_to_xml   : idtable -> XML.tree
    5.54  
    5.55      (* Values as XML strings *)
    5.56 -    val read_pgipint	   : (int option * int option) -> string -> int (* raises PGIP *)
    5.57 -    val read_pgipnat	   : string -> int			        (* raises PGIP *)
    5.58 -    val read_pgipbool	   : string -> bool			        (* raises PGIP *)
    5.59 -    val read_pgipstring	   : string -> string			        (* raises PGIP *)
    5.60 -    val int_to_pgstring	   : int -> string
    5.61 +    val read_pgipint       : (int option * int option) -> string -> int (* raises PGIP *)
    5.62 +    val read_pgipnat       : string -> int                              (* raises PGIP *)
    5.63 +    val read_pgipbool      : string -> bool                             (* raises PGIP *)
    5.64 +    val read_pgipstring    : string -> string                           (* raises PGIP *)
    5.65 +    val int_to_pgstring    : int -> string
    5.66      val bool_to_pgstring   : bool -> string
    5.67      val string_to_pgstring : string -> string
    5.68  
    5.69      (* PGIP datatypes *)
    5.70      val pgiptype_to_xml   : pgiptype -> XML.tree
    5.71 -    val read_pgval        : pgiptype -> string -> pgipval	       (* raises PGIP *)
    5.72 +    val read_pgval        : pgiptype -> string -> pgipval              (* raises PGIP *)
    5.73      val pgval_to_string   : pgipval -> string
    5.74  
    5.75      val attrs_of_displayarea : displayarea -> XML.attributes
    5.76 @@ -88,8 +88,8 @@
    5.77  
    5.78      val haspref : preference -> XML.tree
    5.79  
    5.80 -    val pgipurl_of_url : Url.T -> pgipurl	       (* raises PGIP *)
    5.81 -    val pgipurl_of_string : string -> pgipurl	       (* raises PGIP *)
    5.82 +    val pgipurl_of_url : Url.T -> pgipurl              (* raises PGIP *)
    5.83 +    val pgipurl_of_string : string -> pgipurl          (* raises PGIP *)
    5.84      val pgipurl_of_path : Path.T -> pgipurl
    5.85      val path_of_pgipurl : pgipurl -> Path.T
    5.86      val string_of_pgipurl : pgipurl -> string
    5.87 @@ -98,7 +98,7 @@
    5.88  
    5.89      (* XML utils, only for PGIP code *)
    5.90      val has_attr       : string -> XML.attributes -> bool
    5.91 -    val attr	       : string -> string -> XML.attributes
    5.92 +    val attr           : string -> string -> XML.attributes
    5.93      val opt_attr       : string -> string option -> XML.attributes
    5.94      val opt_attr_map   : ('a -> string) -> string -> 'a option -> XML.attributes
    5.95      val get_attr       : string -> XML.attributes -> string           (* raises PGIP *)
    5.96 @@ -137,11 +137,11 @@
    5.97  (** Objtypes **)
    5.98  
    5.99  datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment  
   5.100 -		 | ObjTerm | ObjType | ObjOther of string
   5.101 +                 | ObjTerm | ObjType | ObjOther of string
   5.102  
   5.103  fun name_of_objtype obj = 
   5.104      case obj of 
   5.105 -	ObjFile    => "file"
   5.106 +        ObjFile    => "file"
   5.107        | ObjTheory  => "theory"
   5.108        | ObjTheorem => "theorem"
   5.109        | ObjComment => "comment"
   5.110 @@ -183,7 +183,7 @@
   5.111  
   5.112  fun read_pgipbool s =
   5.113      (case s of 
   5.114 -	 "false" => false 
   5.115 +         "false" => false 
   5.116         | "true" => true 
   5.117         | _ => raise PGIP ("Invalid boolean value: " ^ quote s))
   5.118  
   5.119 @@ -195,21 +195,21 @@
   5.120  in
   5.121  fun read_pgipint range s =
   5.122      (case Int.fromString s of 
   5.123 -	 SOME i => if int_in_range range i then i
   5.124 -		   else raise PGIP ("Out of range integer value: " ^ quote s)
   5.125 +         SOME i => if int_in_range range i then i
   5.126 +                   else raise PGIP ("Out of range integer value: " ^ quote s)
   5.127         | NONE => raise PGIP ("Invalid integer value: " ^ quote s))
   5.128  end;
   5.129  
   5.130  fun read_pgipnat s =
   5.131      (case Int.fromString s of 
   5.132 -	 SOME i => if i >= 0 then i
   5.133 +         SOME i => if i >= 0 then i
   5.134                     else raise PGIP ("Invalid natural number: " ^ quote s)
   5.135         | NONE => raise PGIP ("Invalid natural number: " ^ quote s))
   5.136  
   5.137  (* NB: we can maybe do without xml decode/encode here. *)
   5.138  fun read_pgipstring s =  (* non-empty strings, XML escapes decoded *)
   5.139      (case XML.parse_string s of
   5.140 -	 SOME s => s
   5.141 +         SOME s => s
   5.142         | NONE => raise PGIP ("Expected a non-empty string: " ^ quote s))
   5.143      handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s)
   5.144  
   5.145 @@ -237,53 +237,53 @@
   5.146  
   5.147  
   5.148  datatype pgiptype = 
   5.149 -	 Pgipnull			     (* unit type: unique element is empty string *)
   5.150 -       | Pgipbool			     (* booleans: "true" or "false" *)
   5.151 +         Pgipnull                            (* unit type: unique element is empty string *)
   5.152 +       | Pgipbool                            (* booleans: "true" or "false" *)
   5.153         | Pgipint of int option * int option  (* ranged integers, should be XSD canonical *)
   5.154 -       | Pgipnat			     (* naturals: non-negative integers (convenience) *)
   5.155 -       | Pgipstring			     (* non-empty strings *)
   5.156 -       | Pgipconst of string		     (* singleton type *)
   5.157 -       | Pgipchoice of pgipdtype list	     (* union type *)
   5.158 +       | Pgipnat                             (* naturals: non-negative integers (convenience) *)
   5.159 +       | Pgipstring                          (* non-empty strings *)
   5.160 +       | Pgipconst of string                 (* singleton type *)
   5.161 +       | Pgipchoice of pgipdtype list        (* union type *)
   5.162  
   5.163  (* Compared with the PGIP schema, we push descriptions of types inside choices. *)
   5.164  
   5.165  and pgipdtype = Pgipdtype of string option * pgiptype
   5.166  
   5.167  datatype pgipuval = Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int 
   5.168 -		  | Pgvalstring of string | Pgvalconst of string
   5.169 +                  | Pgvalstring of string | Pgvalconst of string
   5.170  
   5.171 -type pgipval = pgiptype * pgipuval	(* type-safe values *)
   5.172 +type pgipval = pgiptype * pgipuval      (* type-safe values *)
   5.173  
   5.174  fun pgipdtype_to_xml (desco,ty) = 
   5.175      let
   5.176 -	val desc_attr = opt_attr "descr" desco
   5.177 +        val desc_attr = opt_attr "descr" desco
   5.178  
   5.179 -	val elt = case ty of
   5.180 -		      Pgipnull => "pgipnull"
   5.181 -		    | Pgipbool => "pgipbool"
   5.182 -		    | Pgipint _ => "pgipint"
   5.183 -		    | Pgipnat => "pgipint"
   5.184 -		    | Pgipstring => "pgipstring"
   5.185 -		    | Pgipconst _ => "pgipconst"
   5.186 -		    | Pgipchoice _ => "pgipchoice"
   5.187 +        val elt = case ty of
   5.188 +                      Pgipnull => "pgipnull"
   5.189 +                    | Pgipbool => "pgipbool"
   5.190 +                    | Pgipint _ => "pgipint"
   5.191 +                    | Pgipnat => "pgipint"
   5.192 +                    | Pgipstring => "pgipstring"
   5.193 +                    | Pgipconst _ => "pgipconst"
   5.194 +                    | Pgipchoice _ => "pgipchoice"
   5.195  
   5.196 -	fun range_attr r v = attr r (int_to_pgstring v)
   5.197 +        fun range_attr r v = attr r (int_to_pgstring v)
   5.198  
   5.199 -	val attrs = case ty of 
   5.200 -			Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max)
   5.201 -		      | Pgipint (SOME min,NONE) => (range_attr "min" min)
   5.202 -		      | Pgipint (NONE,SOME max) => (range_attr "max" max)
   5.203 -		      | Pgipnat => (range_attr "min" 0)
   5.204 -		      | Pgipconst nm => attr "name" nm
   5.205 -		      | _ => []
   5.206 +        val attrs = case ty of 
   5.207 +                        Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max)
   5.208 +                      | Pgipint (SOME min,NONE) => (range_attr "min" min)
   5.209 +                      | Pgipint (NONE,SOME max) => (range_attr "max" max)
   5.210 +                      | Pgipnat => (range_attr "min" 0)
   5.211 +                      | Pgipconst nm => attr "name" nm
   5.212 +                      | _ => []
   5.213  
   5.214 -	fun destpgipdtype (Pgipdtype x) = x
   5.215 +        fun destpgipdtype (Pgipdtype x) = x
   5.216  
   5.217 -	val typargs = case ty of
   5.218 -			  Pgipchoice ds => map destpgipdtype ds
   5.219 -			| _ => []
   5.220 +        val typargs = case ty of
   5.221 +                          Pgipchoice ds => map destpgipdtype ds
   5.222 +                        | _ => []
   5.223      in 
   5.224 -	XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
   5.225 +        XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
   5.226      end
   5.227  
   5.228  val pgiptype_to_xml = pgipdtype_to_xml o pair NONE
   5.229 @@ -302,18 +302,18 @@
   5.230      else raise PGIP ("Expecting non-empty string, empty string illegal.")
   5.231    | read_pguval (Pgipchoice tydescs) s = 
   5.232      let 
   5.233 -	(* Union type: match first in list *)
   5.234 -	fun getty (Pgipdtype(_, ty)) = ty
   5.235 -	val uval = get_first 
   5.236 -		       (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
   5.237 -		       (map getty tydescs)
   5.238 +        (* Union type: match first in list *)
   5.239 +        fun getty (Pgipdtype(_, ty)) = ty
   5.240 +        val uval = get_first 
   5.241 +                       (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
   5.242 +                       (map getty tydescs)
   5.243      in
   5.244 -	case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^quote s^
   5.245 -							   " against any allowed types.")
   5.246 +        case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^quote s^
   5.247 +                                                           " against any allowed types.")
   5.248      end
   5.249  
   5.250  fun read_pgval ty s = (ty, read_pguval ty s)
   5.251 -	    
   5.252 +            
   5.253  fun pgval_to_string (_, Pgvalnull) = ""
   5.254    | pgval_to_string (_, Pgvalbool b) = bool_to_pgstring b
   5.255    | pgval_to_string (_, Pgvalnat n) = int_to_pgstring n
   5.256 @@ -329,11 +329,11 @@
   5.257  datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug
   5.258  
   5.259  type location = { descr: string option,
   5.260 -		  url: pgipurl option,
   5.261 -		  line: int option,
   5.262 -		  column: int option,
   5.263 -		  char: int option,
   5.264 -		  length: int option }
   5.265 +                  url: pgipurl option,
   5.266 +                  line: int option,
   5.267 +                  column: int option,
   5.268 +                  char: int option,
   5.269 +                  length: int option }
   5.270  
   5.271  
   5.272  
   5.273 @@ -341,10 +341,10 @@
   5.274  
   5.275  
   5.276  fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
   5.277 -	case Url.explode url of
   5.278 +        case Url.explode url of
   5.279              (Url.File path) => path
   5.280 -	  | _ => raise PGIP ("Cannot access non-local URL " ^ quote url)
   5.281 -		       
   5.282 +          | _ => raise PGIP ("Cannot access non-local URL " ^ quote url)
   5.283 +                       
   5.284  fun pgipurl_of_path p = p
   5.285  
   5.286  fun path_of_pgipurl p = p  (* potentially raises PGIP, but not with this implementation *)
   5.287 @@ -385,51 +385,51 @@
   5.288  
   5.289    fun attrs_of_location ({ descr, url, line, column, char, length }:location) =
   5.290        let 
   5.291 -	  val descr = opt_attr "location_descr" descr
   5.292 -	  val url = opt_attr_map attrval_of_pgipurl "location_url" url
   5.293 -	  val line = opt_attr_map int_to_pgstring "locationline" line
   5.294 -	  val column = opt_attr_map int_to_pgstring "locationcolumn"  column
   5.295 -	  val char = opt_attr_map int_to_pgstring "locationcharacter" char
   5.296 -	  val length = opt_attr_map int_to_pgstring "locationlength" length
   5.297 +          val descr = opt_attr "location_descr" descr
   5.298 +          val url = opt_attr_map attrval_of_pgipurl "location_url" url
   5.299 +          val line = opt_attr_map int_to_pgstring "locationline" line
   5.300 +          val column = opt_attr_map int_to_pgstring "locationcolumn"  column
   5.301 +          val char = opt_attr_map int_to_pgstring "locationcharacter" char
   5.302 +          val length = opt_attr_map int_to_pgstring "locationlength" length
   5.303        in 
   5.304 -	  descr @ url @ line @ column @ char @ length
   5.305 +          descr @ url @ line @ column @ char @ length
   5.306        end
   5.307  
   5.308      fun pgipint_of_string err s = 
   5.309 -	case Int.fromString s of 
   5.310 -	    SOME i => i
   5.311 -	  | NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.")
   5.312 +        case Int.fromString s of 
   5.313 +            SOME i => i
   5.314 +          | NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.")
   5.315  
   5.316    fun location_of_attrs attrs = 
   5.317        let
   5.318 -	  val descr = get_attr_opt "location_descr" attrs
   5.319 -	  val url = Option.map  pgipurl_of_string (get_attr_opt "location_url" attrs)
   5.320 -	  val line = Option.map (pgipint_of_string "location element line attribute")
   5.321 -				(get_attr_opt "locationline" attrs)
   5.322 -	  val column = Option.map (pgipint_of_string "location element column attribute")
   5.323 -				  (get_attr_opt "locationcolumn" attrs)
   5.324 -	  val char = Option.map (pgipint_of_string "location element char attribute")
   5.325 -				(get_attr_opt "locationcharacter" attrs)
   5.326 -	  val length = Option.map (pgipint_of_string "location element length attribute")
   5.327 -				  (get_attr_opt "locationlength" attrs)
   5.328 +          val descr = get_attr_opt "location_descr" attrs
   5.329 +          val url = Option.map  pgipurl_of_string (get_attr_opt "location_url" attrs)
   5.330 +          val line = Option.map (pgipint_of_string "location element line attribute")
   5.331 +                                (get_attr_opt "locationline" attrs)
   5.332 +          val column = Option.map (pgipint_of_string "location element column attribute")
   5.333 +                                  (get_attr_opt "locationcolumn" attrs)
   5.334 +          val char = Option.map (pgipint_of_string "location element char attribute")
   5.335 +                                (get_attr_opt "locationcharacter" attrs)
   5.336 +          val length = Option.map (pgipint_of_string "location element length attribute")
   5.337 +                                  (get_attr_opt "locationlength" attrs)
   5.338        in 
   5.339 -	  {descr=descr, url=url, line=line, column=column, char=char, length=length}
   5.340 +          {descr=descr, url=url, line=line, column=column, char=char, length=length}
   5.341        end
   5.342  end
   5.343  
   5.344  (** Preferences **)
   5.345  
   5.346  type preference = { name: string,
   5.347 -		    descr: string option,
   5.348 -		    default: string option,
   5.349 -		    pgiptype: pgiptype }
   5.350 +                    descr: string option,
   5.351 +                    default: string option,
   5.352 +                    pgiptype: pgiptype }
   5.353  
   5.354  fun haspref ({ name, descr, default, pgiptype}:preference) = 
   5.355      XML.Elem ("haspref",
   5.356 -	      attr "name" name @
   5.357 -	      opt_attr "descr" descr @
   5.358 -	      opt_attr "default" default,
   5.359 -	      [pgiptype_to_xml pgiptype])
   5.360 +              attr "name" name @
   5.361 +              opt_attr "descr" descr @
   5.362 +              opt_attr "default" default,
   5.363 +              [pgiptype_to_xml pgiptype])
   5.364  
   5.365  end
   5.366  
     6.1 --- a/src/Pure/ProofGeneral/pgml.ML	Wed Aug 27 11:49:50 2008 +0200
     6.2 +++ b/src/Pure/ProofGeneral/pgml.ML	Wed Aug 27 12:00:28 2008 +0200
     6.3 @@ -18,29 +18,29 @@
     6.4      datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
     6.5  
     6.6      datatype pgmlaction = Toggle | Button | Menu
     6.7 -					    
     6.8 +                                            
     6.9      datatype pgmlterm = 
    6.10 -	     Atoms of { kind: string option, content: pgmlatom list }
    6.11 -	   | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
    6.12 -	   | Break of { mandatory: bool option, indent: int option }
    6.13 -	   | Subterm of { kind: string option,
    6.14 -			  param: string option,
    6.15 -			  place: pgmlplace option,
    6.16 -			  name: string option,
    6.17 -			  decoration: pgmldec option,
    6.18 -			  action: pgmlaction option,
    6.19 -			  pos: string option,
    6.20 -			  xref: PgipTypes.pgipurl option,
    6.21 -			  content: pgmlterm list }
    6.22 -	   | Alt of { kind: string option, content: pgmlterm list }
    6.23 -	   | Embed of XML.tree list
    6.24 -	   | Raw of XML.tree
    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 +             Pgml of { version: string option, systemid: string option, 
    6.47 +                       area: PgipTypes.displayarea option, 
    6.48 +                       content: pgmlterm list }
    6.49 +                       
    6.50      val pgmlterm_to_xml : pgmlterm -> XML.tree
    6.51  
    6.52      val pgml_to_xml : pgml -> XML.tree
    6.53 @@ -62,29 +62,29 @@
    6.54      datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
    6.55  
    6.56      datatype pgmlaction = Toggle | Button | Menu
    6.57 -					    
    6.58 +                                            
    6.59      datatype pgmlterm = 
    6.60 -	     Atoms of { kind: string option, content: pgmlatom list }
    6.61 -	   | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
    6.62 -	   | Break of { mandatory: bool option, indent: int option }
    6.63 -	   | Subterm of { kind: string option,
    6.64 -			  param: string option,
    6.65 -			  place: pgmlplace option,
    6.66 -			  name: string option,
    6.67 -			  decoration: pgmldec option,
    6.68 -			  action: pgmlaction option,
    6.69 -			  pos: string option,
    6.70 -			  xref: PgipTypes.pgipurl option,
    6.71 -			  content: pgmlterm list }
    6.72 -	   | Alt of { kind: string option, content: pgmlterm list }
    6.73 -	   | Embed of XML.tree list
    6.74 -	   | Raw of XML.tree
    6.75 +             Atoms of { kind: string option, content: pgmlatom list }
    6.76 +           | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
    6.77 +           | Break of { mandatory: bool option, indent: int option }
    6.78 +           | Subterm of { kind: string option,
    6.79 +                          param: string option,
    6.80 +                          place: pgmlplace option,
    6.81 +                          name: string option,
    6.82 +                          decoration: pgmldec option,
    6.83 +                          action: pgmlaction option,
    6.84 +                          pos: string option,
    6.85 +                          xref: PgipTypes.pgipurl option,
    6.86 +                          content: pgmlterm list }
    6.87 +           | Alt of { kind: string option, content: pgmlterm list }
    6.88 +           | Embed of XML.tree list
    6.89 +           | Raw of XML.tree
    6.90  
    6.91 -		       
    6.92 +                       
    6.93      datatype pgml = 
    6.94 -	     Pgml of { version: string option, systemid: string option, 
    6.95 -		       area: PgipTypes.displayarea option, 
    6.96 -		       content: pgmlterm list }
    6.97 +             Pgml of { version: string option, systemid: string option, 
    6.98 +                       area: PgipTypes.displayarea option, 
    6.99 +                       content: pgmlterm list }
   6.100  
   6.101      fun pgmlorient_to_string HOVOrient = "hov"
   6.102        | pgmlorient_to_string HOrient = "h"
   6.103 @@ -111,35 +111,35 @@
   6.104         would be better not to *)
   6.105      fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content])
   6.106        | atom_to_xml (Str str) = XML.Output str 
   6.107 -						    
   6.108 +                                                    
   6.109      fun pgmlterm_to_xml (Atoms {kind, content}) = 
   6.110 -	XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
   6.111 +        XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
   6.112  
   6.113        | pgmlterm_to_xml (Box {orient, indent, content}) =
   6.114 -	XML.Elem("box", 
   6.115 -		 opt_attr_map pgmlorient_to_string "orient" orient @
   6.116 -		 opt_attr_map int_to_pgstring "indent" indent,
   6.117 -		 map pgmlterm_to_xml content)
   6.118 +        XML.Elem("box", 
   6.119 +                 opt_attr_map pgmlorient_to_string "orient" orient @
   6.120 +                 opt_attr_map int_to_pgstring "indent" indent,
   6.121 +                 map pgmlterm_to_xml content)
   6.122  
   6.123        | pgmlterm_to_xml (Break {mandatory, indent}) =
   6.124 -	XML.Elem("break",
   6.125 -		 opt_attr_map bool_to_pgstring "mandatory" mandatory @
   6.126 -		 opt_attr_map int_to_pgstring "indent" indent, [])
   6.127 +        XML.Elem("break",
   6.128 +                 opt_attr_map bool_to_pgstring "mandatory" mandatory @
   6.129 +                 opt_attr_map int_to_pgstring "indent" indent, [])
   6.130  
   6.131        | pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
   6.132 -	XML.Elem("subterm", 
   6.133 -  		 opt_attr "kind" kind @
   6.134 -		 opt_attr "param" param @
   6.135 -		 opt_attr_map pgmlplace_to_string "place" place @
   6.136 -		 opt_attr "name" name @ 
   6.137 -		 opt_attr_map pgmldec_to_string "decoration" decoration @
   6.138 -		 opt_attr_map pgmlaction_to_string "action" action @ 
   6.139 -		 opt_attr "pos" pos @
   6.140 -		 opt_attr_map string_of_pgipurl "xref" xref,
   6.141 -		 map pgmlterm_to_xml content)
   6.142 +        XML.Elem("subterm", 
   6.143 +                 opt_attr "kind" kind @
   6.144 +                 opt_attr "param" param @
   6.145 +                 opt_attr_map pgmlplace_to_string "place" place @
   6.146 +                 opt_attr "name" name @ 
   6.147 +                 opt_attr_map pgmldec_to_string "decoration" decoration @
   6.148 +                 opt_attr_map pgmlaction_to_string "action" action @ 
   6.149 +                 opt_attr "pos" pos @
   6.150 +                 opt_attr_map string_of_pgipurl "xref" xref,
   6.151 +                 map pgmlterm_to_xml content)
   6.152  
   6.153        | pgmlterm_to_xml (Alt {kind, content}) = 
   6.154 -	XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
   6.155 +        XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
   6.156  
   6.157        | pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
   6.158  
   6.159 @@ -147,14 +147,14 @@
   6.160  
   6.161  
   6.162      datatype pgml = 
   6.163 -	     Pgml of { version: string option, systemid: string option, 
   6.164 -		       area: PgipTypes.displayarea option, 
   6.165 -		       content: pgmlterm list }
   6.166 +             Pgml of { version: string option, systemid: string option, 
   6.167 +                       area: PgipTypes.displayarea option, 
   6.168 +                       content: pgmlterm list }
   6.169  
   6.170      fun pgml_to_xml (Pgml {version,systemid,area,content}) = 
   6.171 -	XML.Elem("pgml",
   6.172 -		 opt_attr "version" version @ 
   6.173 -		 opt_attr "systemid" systemid @
   6.174 -		 Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
   6.175 -		 map pgmlterm_to_xml content)
   6.176 +        XML.Elem("pgml",
   6.177 +                 opt_attr "version" version @ 
   6.178 +                 opt_attr "systemid" systemid @
   6.179 +                 Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
   6.180 +                 map pgmlterm_to_xml content)
   6.181  end
     7.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Aug 27 11:49:50 2008 +0200
     7.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Aug 27 12:00:28 2008 +0200
     7.3 @@ -178,7 +178,7 @@
     7.4      let
     7.5        val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
     7.6        val deps = Symtab.keys (fold Proofterm.thms_of_proof'
     7.7 -				   (map Thm.proof_of ths) Symtab.empty);
     7.8 +                                   (map Thm.proof_of ths) Symtab.empty);
     7.9      in
    7.10        if null names orelse null deps then ()
    7.11        else thm_deps_message (spaces_quote names, spaces_quote deps)
     8.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Aug 27 11:49:50 2008 +0200
     8.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Aug 27 12:00:28 2008 +0200
     8.3 @@ -763,7 +763,7 @@
     8.4          val location = #location vs   (* TODO: extract position *)
     8.5  
     8.6          val _ = start_delay_msgs ()   (* gather parsing errs/warns *)
     8.7 -		    val doc = PgipParser.pgip_parser Position.none text
     8.8 +        val doc = PgipParser.pgip_parser Position.none text
     8.9          val errs = end_delayed_msgs ()
    8.10  
    8.11          val sysattrs = PgipTypes.opt_attr "systemdata" systemdata