# HG changeset patch
# User wenzelm
# Date 1219831228 -7200
# Node ID 1ff5167592baf14a7b03185b11c4f786e2d9306b
# Parent 359764333bf41747048ceb635875508ea82d535d
get rid of tabs;
diff -r 359764333bf4 -r 1ff5167592ba src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/Isar/locale.ML Wed Aug 27 12:00:28 2008 +0200
@@ -1595,10 +1595,10 @@
val id' = prep_id id
val eqns' = case get_reg id'
of NONE => eqns
- | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
+ | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
handle Termtab.DUP t =>
- error ("Conflicting interpreting equations for term " ^
- quote (Syntax.string_of_term ctxt t))
+ error ("Conflicting interpreting equations for term " ^
+ quote (Syntax.string_of_term ctxt t))
in ((id', eqns'), eqns') end;
diff -r 359764333bf4 -r 1ff5167592ba src/Pure/ProofGeneral/pgip_input.ML
--- a/src/Pure/ProofGeneral/pgip_input.ML Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_input.ML Wed Aug 27 12:00:28 2008 +0200
@@ -30,15 +30,15 @@
| Restoregoal of { thmname : string }
(* context inspection commands *)
| Askids of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option }
+ thyname: PgipTypes.objname option,
+ objtype: PgipTypes.objtype option }
| Askrefs of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option,
- name: PgipTypes.objname option }
+ thyname: PgipTypes.objname option,
+ objtype: PgipTypes.objtype option,
+ name: PgipTypes.objname option }
| Showid of { thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype,
- name: PgipTypes.objname }
+ objtype: PgipTypes.objtype,
+ name: PgipTypes.objname }
| Askguise of { }
| Parsescript of { text: string, location: PgipTypes.location,
systemdata: string option }
@@ -74,59 +74,59 @@
(*** PGIP input ***)
datatype pgipinput =
- (* protocol/prover config *)
- Askpgip of { }
- | Askpgml of { }
- | Askconfig of { }
- | Askprefs of { }
- | Setpref of { name:string, prefcategory:string option, value:string }
- | Getpref of { name:string, prefcategory:string option }
+ (* protocol/prover config *)
+ Askpgip of { }
+ | Askpgml of { }
+ | Askconfig of { }
+ | Askprefs of { }
+ | Setpref of { name:string, prefcategory:string option, value:string }
+ | Getpref of { name:string, prefcategory:string option }
(* prover control *)
- | Proverinit of { }
- | Proverexit of { }
+ | Proverinit of { }
+ | Proverexit of { }
| Setproverflag of { flagname:string, value: bool }
(* improper proof commands: control proof state *)
- | Dostep of { text: string }
- | Undostep of { times: int }
- | Redostep of { }
- | Abortgoal of { }
- | Forget of { thyname: string option, name: string option,
- objtype: PgipTypes.objtype option }
+ | Dostep of { text: string }
+ | Undostep of { times: int }
+ | Redostep of { }
+ | Abortgoal of { }
+ | Forget of { thyname: string option, name: string option,
+ objtype: PgipTypes.objtype option }
| Restoregoal of { thmname : string }
(* context inspection commands *)
| Askids of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option }
+ thyname: PgipTypes.objname option,
+ objtype: PgipTypes.objtype option }
| Askrefs of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option,
- name: PgipTypes.objname option }
+ thyname: PgipTypes.objname option,
+ objtype: PgipTypes.objtype option,
+ name: PgipTypes.objname option }
| Showid of { thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype,
- name: PgipTypes.objname }
- | Askguise of { }
- | Parsescript of { text: string, location: location,
- systemdata: string option }
+ objtype: PgipTypes.objtype,
+ name: PgipTypes.objname }
+ | Askguise of { }
+ | Parsescript of { text: string, location: location,
+ systemdata: string option }
| Showproofstate of { }
- | Showctxt of { }
+ | Showctxt of { }
| Searchtheorems of { arg: string }
| Setlinewidth of { width: int }
- | Viewdoc of { arg: string }
+ | Viewdoc of { arg: string }
(* improper theory-level commands *)
- | Doitem of { text: string }
- | Undoitem of { }
- | Redoitem of { }
- | Aborttheory of { }
+ | Doitem of { text: string }
+ | Undoitem of { }
+ | Redoitem of { }
+ | Aborttheory of { }
| Retracttheory of { thyname: string }
- | Loadfile of { url: pgipurl }
- | Openfile of { url: pgipurl }
- | Closefile of { }
- | Abortfile of { }
+ | Loadfile of { url: pgipurl }
+ | Openfile of { url: pgipurl }
+ | Closefile of { }
+ | Abortfile of { }
| Retractfile of { url: pgipurl }
- | Changecwd of { url: pgipurl }
- | Systemcmd of { arg: string }
+ | Changecwd of { url: pgipurl }
+ | Systemcmd of { arg: string }
(* unofficial escape command for debugging *)
- | Quitpgip of { }
+ | Quitpgip of { }
(* Extracting content from input XML elements to make a PGIPinput *)
local
@@ -140,12 +140,12 @@
val value_attr = get_attr "value"
fun objtype_attro attrs = if has_attr "objtype" attrs then
- SOME (objtype_of_attrs attrs)
- else NONE
+ SOME (objtype_of_attrs attrs)
+ else NONE
fun pgipurl_attro attrs = if has_attr "url" attrs then
- SOME (pgipurl_of_attrs attrs)
- else NONE
+ SOME (pgipurl_of_attrs attrs)
+ else NONE
val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
val prefcat_attr = get_attr_opt "prefcategory"
@@ -171,39 +171,39 @@
(* proverconfig *)
| "askprefs" => Askprefs { }
| "getpref" => Getpref { name = name_attr attrs,
- prefcategory = prefcat_attr attrs }
+ prefcategory = prefcat_attr attrs }
| "setpref" => Setpref { name = name_attr attrs,
- prefcategory = prefcat_attr attrs,
- value = xmltext data }
+ prefcategory = prefcat_attr attrs,
+ value = xmltext data }
(* provercontrol *)
| "proverinit" => Proverinit { }
| "proverexit" => Proverexit { }
| "setproverflag" => Setproverflag { flagname = flagname_attr attrs,
- value = read_pgipbool (value_attr attrs) }
+ value = read_pgipbool (value_attr attrs) }
(* improperproofcmd: improper commands not in script *)
| "dostep" => Dostep { text = xmltext data }
| "undostep" => Undostep { times = times_attr attrs }
| "redostep" => Redostep { }
| "abortgoal" => Abortgoal { }
| "forget" => Forget { thyname = thyname_attro attrs,
- name = name_attro attrs,
- objtype = objtype_attro attrs }
+ name = name_attro attrs,
+ objtype = objtype_attro attrs }
| "restoregoal" => Restoregoal { thmname = thmname_attr attrs}
(* proofctxt: improper commands *)
| "askids" => Askids { url = pgipurl_attro attrs,
- thyname = thyname_attro attrs,
- objtype = objtype_attro attrs }
+ thyname = thyname_attro attrs,
+ objtype = objtype_attro attrs }
| "askrefs" => Askrefs { url = pgipurl_attro attrs,
- thyname = thyname_attro attrs,
- objtype = objtype_attro attrs,
- name = name_attro attrs }
+ thyname = thyname_attro attrs,
+ objtype = objtype_attro attrs,
+ name = name_attro attrs }
| "showid" => Showid { thyname = thyname_attro attrs,
- objtype = objtype_of_attrs attrs,
- name = name_attr attrs }
+ objtype = objtype_of_attrs attrs,
+ name = name_attr attrs }
| "askguise" => Askguise { }
| "parsescript" => Parsescript { text = (xmltext data),
- systemdata = get_attr_opt "systemdata" attrs,
- location = location_of_attrs attrs }
+ systemdata = get_attr_opt "systemdata" attrs,
+ location = location_of_attrs attrs }
| "showproofstate" => Showproofstate { }
| "showctxt" => Showctxt { }
| "searchtheorems" => Searchtheorems { arg = xmltext data }
@@ -223,17 +223,17 @@
| "changecwd" => Changecwd { url = pgipurl_of_attrs attrs }
| "systemcmd" => Systemcmd { arg = xmltext data }
(* unofficial command for debugging *)
- | "quitpgip" => Quitpgip { }
+ | "quitpgip" => Quitpgip { }
(* We allow sending proper document markup too; we map it back to dostep *)
(* and strip out metainfo elements. Markup correctness isn't checked: this *)
(* is a compatibility measure to make it easy for interfaces. *)
| x => if (x mem PgipMarkup.doc_markup_elements) then
- if (x mem PgipMarkup.doc_markup_elements_ignored) then
- raise NoAction
- else
- Dostep { text = xmltext data } (* could separate out Doitem too *)
- else raise Unknown)
+ if (x mem PgipMarkup.doc_markup_elements_ignored) then
+ raise NoAction
+ else
+ Dostep { text = xmltext data } (* could separate out Doitem too *)
+ else raise Unknown)
handle Unknown => NONE | NoAction => NONE
end
diff -r 359764333bf4 -r 1ff5167592ba src/Pure/ProofGeneral/pgip_output.ML
--- a/src/Pure/ProofGeneral/pgip_output.ML Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML Wed Aug 27 12:00:28 2008 +0200
@@ -32,21 +32,21 @@
prefs: PgipTypes.preference list }
| Prefval of { name: string, value: string }
| Setrefs of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option,
- name: PgipTypes.objname option,
- idtables: PgipTypes.idtable list,
- fileurls : PgipTypes.pgipurl list }
+ thyname: PgipTypes.objname option,
+ objtype: PgipTypes.objtype option,
+ name: PgipTypes.objname option,
+ idtables: PgipTypes.idtable list,
+ fileurls : PgipTypes.pgipurl list }
| Idvalue of { thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype,
- name: PgipTypes.objname,
- text: XML.tree list }
+ objtype: PgipTypes.objtype,
+ name: PgipTypes.objname,
+ text: XML.tree list }
| Informguise of { file : PgipTypes.pgipurl option,
theory: PgipTypes.objname option,
theorem: PgipTypes.objname option,
proofpos: int option }
| Parseresult of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument,
- errs: XML.tree list } (* errs to become PGML *)
+ errs: XML.tree list } (* errs to become PGML *)
| Usespgip of { version: string,
pgipelems: (string * bool * string list) list }
| Usespgml of { version: string }
@@ -67,10 +67,10 @@
open PgipTypes
datatype pgipoutput =
- Normalresponse of { content: XML.tree list }
+ Normalresponse of { content: XML.tree list }
| Errorresponse of { fatality: fatality,
location: location option,
- content: XML.tree list }
+ content: XML.tree list }
| Informfileloaded of { url: Path.T, completed: bool }
| Informfileoutdated of { url: Path.T, completed: bool }
| Informfileretracted of { url: Path.T, completed: bool }
@@ -84,21 +84,21 @@
| Hasprefs of { prefcategory: string option, prefs: preference list }
| Prefval of { name: string, value: string }
| Idvalue of { thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype,
- name: PgipTypes.objname,
- text: XML.tree list }
+ objtype: PgipTypes.objtype,
+ name: PgipTypes.objname,
+ text: XML.tree list }
| Setrefs of { url: PgipTypes.pgipurl option,
- thyname: PgipTypes.objname option,
- objtype: PgipTypes.objtype option,
- name: PgipTypes.objname option,
- idtables: PgipTypes.idtable list,
- fileurls : PgipTypes.pgipurl list }
+ thyname: PgipTypes.objname option,
+ objtype: PgipTypes.objtype option,
+ name: PgipTypes.objname option,
+ idtables: PgipTypes.idtable list,
+ fileurls : PgipTypes.pgipurl list }
| Informguise of { file : PgipTypes.pgipurl option,
- theory: PgipTypes.objname option,
- theorem: PgipTypes.objname option,
- proofpos: int option }
+ theory: PgipTypes.objname option,
+ theorem: PgipTypes.objname option,
+ proofpos: int option }
| Parseresult of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
- errs: XML.tree list } (* errs to become PGML *)
+ errs: XML.tree list } (* errs to become PGML *)
| Usespgip of { version: string,
pgipelems: (string * bool * string list) list }
| Usespgml of { version: string }
@@ -119,7 +119,7 @@
val content = #content vs
in
XML.Elem ("normalresponse",
- [],
+ [],
content)
end
@@ -141,9 +141,9 @@
val completed = #completed vs
in
XML.Elem ("informfileloaded",
- attrs_of_pgipurl url @
- (attr "completed" (PgipTypes.bool_to_pgstring completed)),
- [])
+ attrs_of_pgipurl url @
+ (attr "completed" (PgipTypes.bool_to_pgstring completed)),
+ [])
end
fun informfileoutdated (Informfileoutdated vs) =
@@ -152,9 +152,9 @@
val completed = #completed vs
in
XML.Elem ("informfileoutdated",
- attrs_of_pgipurl url @
- (attr "completed" (PgipTypes.bool_to_pgstring completed)),
- [])
+ attrs_of_pgipurl url @
+ (attr "completed" (PgipTypes.bool_to_pgstring completed)),
+ [])
end
fun informfileretracted (Informfileretracted vs) =
@@ -163,9 +163,9 @@
val completed = #completed vs
in
XML.Elem ("informfileretracted",
- attrs_of_pgipurl url @
- (attr "completed" (PgipTypes.bool_to_pgstring completed)),
- [])
+ attrs_of_pgipurl url @
+ (attr "completed" (PgipTypes.bool_to_pgstring completed)),
+ [])
end
fun metainforesponse (Metainforesponse vs) =
@@ -211,21 +211,21 @@
fun setrefs (Setrefs vs) =
let
- val url = #url vs
- val thyname = #thyname vs
- val objtype = #objtype vs
- val name = #name vs
+ val url = #url vs
+ val thyname = #thyname vs
+ val objtype = #objtype vs
+ val name = #name vs
val idtables = #idtables vs
val fileurls = #fileurls vs
- fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
+ fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
in
XML.Elem ("setrefs",
- (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @
- (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
- (opt_attr "thyname" thyname) @
- (opt_attr "name" name),
- (map idtable_to_xml idtables) @
- (map fileurl_to_xml fileurls))
+ (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @
+ (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
+ (opt_attr "thyname" thyname) @
+ (opt_attr "name" name),
+ (map idtable_to_xml idtables) @
+ (map fileurl_to_xml fileurls))
end
fun addids (Addids vs) =
@@ -260,16 +260,16 @@
fun idvalue (Idvalue vs) =
let
- val objtype_attrs = attrs_of_objtype (#objtype vs)
- val thyname = #thyname vs
+ val objtype_attrs = attrs_of_objtype (#objtype vs)
+ val thyname = #thyname vs
val name = #name vs
val text = #text vs
in
XML.Elem("idvalue",
- objtype_attrs @
- (opt_attr "thyname" thyname) @
- (attr "name" name),
- text)
+ objtype_attrs @
+ (opt_attr "thyname" thyname) @
+ (attr "name" name),
+ text)
end
fun informguise (Informguise vs) =
@@ -295,7 +295,7 @@
val attrs = #attrs vs
val doc = #doc vs
val errs = #errs vs
- val xmldoc = PgipMarkup.output_doc doc
+ val xmldoc = PgipMarkup.output_doc doc
in
XML.Elem("parseresult", attrs, errs @ xmldoc)
end
diff -r 359764333bf4 -r 1ff5167592ba src/Pure/ProofGeneral/pgip_tests.ML
--- a/src/Pure/ProofGeneral/pgip_tests.ML Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_tests.ML Wed Aug 27 12:00:28 2008 +0200
@@ -12,7 +12,7 @@
fun asseq_p toS a b =
if a=b then ()
else error("PGIP test: expected these two values to be equal:\n" ^
- (toS a) ^"\n and: \n" ^ (toS b))
+ (toS a) ^"\n and: \n" ^ (toS b))
val asseqx = asseq_p XML.string_of
val asseqs = asseq_p I
@@ -40,18 +40,18 @@
local
val choices = Pgipchoice [Pgipdtype (NONE,Pgipbool), Pgipdtype (NONE,Pgipnat),
- Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
+ Pgipdtype (NONE,Pgipnull), Pgipdtype (NONE,Pgipconst "foo")]
in
val _ = asseqs (pgval_to_string (read_pgval choices "45")) "45";
val _ = asseqs (pgval_to_string (read_pgval choices "foo")) "foo";
val _ = asseqs (pgval_to_string (read_pgval choices "true")) "true";
val _ = asseqs (pgval_to_string (read_pgval choices "")) "";
val _ = (asseqs (pgval_to_string (read_pgval choices "-37")) "-37";
- error "pgip_tests: should fail") handle PGIP _ => ()
+ error "pgip_tests: should fail") handle PGIP _ => ()
end
val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
- default=SOME "true", pgiptype=Pgipbool})
+ default=SOME "true", pgiptype=Pgipbool})
(XML.parse "");
end
@@ -60,8 +60,8 @@
local
fun e str = case XML.parse str of
- (XML.Elem args) => args
- | _ => error("Expected to get an XML Element")
+ (XML.Elem args) => args
+ | _ => error("Expected to get an XML Element")
open PgipInput;
open PgipTypes;
@@ -83,7 +83,7 @@
val _ = asseqi "" (SOME (Stopquiet()));
*)
val _ = asseqi "" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
- objtype=SOME ObjTheory,name=NONE}));
+ objtype=SOME ObjTheory,name=NONE}));
val _ = asseqi "" NONE;
end
diff -r 359764333bf4 -r 1ff5167592ba src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML Wed Aug 27 12:00:28 2008 +0200
@@ -11,7 +11,7 @@
(* Object types: the types of values which can be manipulated externally.
Ideally a list of other types would be configured as a parameter. *)
datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment
- | ObjTerm | ObjType | ObjOther of string
+ | ObjTerm | ObjType | ObjOther of string
(* Names for values of objtypes (i.e. prover identifiers). Could be a parameter.
Names for ObjFiles are URIs. *)
@@ -24,7 +24,7 @@
(* Types and values (used for preferences and dialogs) *)
datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat
- | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
+ | Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list
and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *)
@@ -44,17 +44,17 @@
(* File location *)
type location = { descr: string option,
- url: pgipurl option,
- line: int option,
- column: int option,
- char: int option,
- length: int option }
+ url: pgipurl option,
+ line: int option,
+ column: int option,
+ char: int option,
+ length: int option }
(* Prover preference *)
type preference = { name: string,
- descr: string option,
- default: string option,
- pgiptype: pgiptype }
+ descr: string option,
+ default: string option,
+ pgiptype: pgiptype }
end
signature PGIPTYPES_OPNS =
@@ -64,21 +64,21 @@
(* Object types *)
val name_of_objtype : objtype -> string
val attrs_of_objtype : objtype -> XML.attributes
- val objtype_of_attrs : XML.attributes -> objtype (* raises PGIP *)
+ val objtype_of_attrs : XML.attributes -> objtype (* raises PGIP *)
val idtable_to_xml : idtable -> XML.tree
(* Values as XML strings *)
- val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *)
- val read_pgipnat : string -> int (* raises PGIP *)
- val read_pgipbool : string -> bool (* raises PGIP *)
- val read_pgipstring : string -> string (* raises PGIP *)
- val int_to_pgstring : int -> string
+ val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *)
+ val read_pgipnat : string -> int (* raises PGIP *)
+ val read_pgipbool : string -> bool (* raises PGIP *)
+ val read_pgipstring : string -> string (* raises PGIP *)
+ val int_to_pgstring : int -> string
val bool_to_pgstring : bool -> string
val string_to_pgstring : string -> string
(* PGIP datatypes *)
val pgiptype_to_xml : pgiptype -> XML.tree
- val read_pgval : pgiptype -> string -> pgipval (* raises PGIP *)
+ val read_pgval : pgiptype -> string -> pgipval (* raises PGIP *)
val pgval_to_string : pgipval -> string
val attrs_of_displayarea : displayarea -> XML.attributes
@@ -88,8 +88,8 @@
val haspref : preference -> XML.tree
- val pgipurl_of_url : Url.T -> pgipurl (* raises PGIP *)
- val pgipurl_of_string : string -> pgipurl (* raises PGIP *)
+ val pgipurl_of_url : Url.T -> pgipurl (* raises PGIP *)
+ val pgipurl_of_string : string -> pgipurl (* raises PGIP *)
val pgipurl_of_path : Path.T -> pgipurl
val path_of_pgipurl : pgipurl -> Path.T
val string_of_pgipurl : pgipurl -> string
@@ -98,7 +98,7 @@
(* XML utils, only for PGIP code *)
val has_attr : string -> XML.attributes -> bool
- val attr : string -> string -> XML.attributes
+ val attr : string -> string -> XML.attributes
val opt_attr : string -> string option -> XML.attributes
val opt_attr_map : ('a -> string) -> string -> 'a option -> XML.attributes
val get_attr : string -> XML.attributes -> string (* raises PGIP *)
@@ -137,11 +137,11 @@
(** Objtypes **)
datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment
- | ObjTerm | ObjType | ObjOther of string
+ | ObjTerm | ObjType | ObjOther of string
fun name_of_objtype obj =
case obj of
- ObjFile => "file"
+ ObjFile => "file"
| ObjTheory => "theory"
| ObjTheorem => "theorem"
| ObjComment => "comment"
@@ -183,7 +183,7 @@
fun read_pgipbool s =
(case s of
- "false" => false
+ "false" => false
| "true" => true
| _ => raise PGIP ("Invalid boolean value: " ^ quote s))
@@ -195,21 +195,21 @@
in
fun read_pgipint range s =
(case Int.fromString s of
- SOME i => if int_in_range range i then i
- else raise PGIP ("Out of range integer value: " ^ quote s)
+ SOME i => if int_in_range range i then i
+ else raise PGIP ("Out of range integer value: " ^ quote s)
| NONE => raise PGIP ("Invalid integer value: " ^ quote s))
end;
fun read_pgipnat s =
(case Int.fromString s of
- SOME i => if i >= 0 then i
+ SOME i => if i >= 0 then i
else raise PGIP ("Invalid natural number: " ^ quote s)
| NONE => raise PGIP ("Invalid natural number: " ^ quote s))
(* NB: we can maybe do without xml decode/encode here. *)
fun read_pgipstring s = (* non-empty strings, XML escapes decoded *)
(case XML.parse_string s of
- SOME s => s
+ SOME s => s
| NONE => raise PGIP ("Expected a non-empty string: " ^ quote s))
handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s)
@@ -237,53 +237,53 @@
datatype pgiptype =
- Pgipnull (* unit type: unique element is empty string *)
- | Pgipbool (* booleans: "true" or "false" *)
+ Pgipnull (* unit type: unique element is empty string *)
+ | Pgipbool (* booleans: "true" or "false" *)
| Pgipint of int option * int option (* ranged integers, should be XSD canonical *)
- | Pgipnat (* naturals: non-negative integers (convenience) *)
- | Pgipstring (* non-empty strings *)
- | Pgipconst of string (* singleton type *)
- | Pgipchoice of pgipdtype list (* union type *)
+ | Pgipnat (* naturals: non-negative integers (convenience) *)
+ | Pgipstring (* non-empty strings *)
+ | Pgipconst of string (* singleton type *)
+ | Pgipchoice of pgipdtype list (* union type *)
(* Compared with the PGIP schema, we push descriptions of types inside choices. *)
and pgipdtype = Pgipdtype of string option * pgiptype
datatype pgipuval = Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int
- | Pgvalstring of string | Pgvalconst of string
+ | Pgvalstring of string | Pgvalconst of string
-type pgipval = pgiptype * pgipuval (* type-safe values *)
+type pgipval = pgiptype * pgipuval (* type-safe values *)
fun pgipdtype_to_xml (desco,ty) =
let
- val desc_attr = opt_attr "descr" desco
+ val desc_attr = opt_attr "descr" desco
- val elt = case ty of
- Pgipnull => "pgipnull"
- | Pgipbool => "pgipbool"
- | Pgipint _ => "pgipint"
- | Pgipnat => "pgipint"
- | Pgipstring => "pgipstring"
- | Pgipconst _ => "pgipconst"
- | Pgipchoice _ => "pgipchoice"
+ val elt = case ty of
+ Pgipnull => "pgipnull"
+ | Pgipbool => "pgipbool"
+ | Pgipint _ => "pgipint"
+ | Pgipnat => "pgipint"
+ | Pgipstring => "pgipstring"
+ | Pgipconst _ => "pgipconst"
+ | Pgipchoice _ => "pgipchoice"
- fun range_attr r v = attr r (int_to_pgstring v)
+ fun range_attr r v = attr r (int_to_pgstring v)
- val attrs = case ty of
- Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max)
- | Pgipint (SOME min,NONE) => (range_attr "min" min)
- | Pgipint (NONE,SOME max) => (range_attr "max" max)
- | Pgipnat => (range_attr "min" 0)
- | Pgipconst nm => attr "name" nm
- | _ => []
+ val attrs = case ty of
+ Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max)
+ | Pgipint (SOME min,NONE) => (range_attr "min" min)
+ | Pgipint (NONE,SOME max) => (range_attr "max" max)
+ | Pgipnat => (range_attr "min" 0)
+ | Pgipconst nm => attr "name" nm
+ | _ => []
- fun destpgipdtype (Pgipdtype x) = x
+ fun destpgipdtype (Pgipdtype x) = x
- val typargs = case ty of
- Pgipchoice ds => map destpgipdtype ds
- | _ => []
+ val typargs = case ty of
+ Pgipchoice ds => map destpgipdtype ds
+ | _ => []
in
- XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
+ XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs))
end
val pgiptype_to_xml = pgipdtype_to_xml o pair NONE
@@ -302,18 +302,18 @@
else raise PGIP ("Expecting non-empty string, empty string illegal.")
| read_pguval (Pgipchoice tydescs) s =
let
- (* Union type: match first in list *)
- fun getty (Pgipdtype(_, ty)) = ty
- val uval = get_first
- (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
- (map getty tydescs)
+ (* Union type: match first in list *)
+ fun getty (Pgipdtype(_, ty)) = ty
+ val uval = get_first
+ (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
+ (map getty tydescs)
in
- case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^quote s^
- " against any allowed types.")
+ case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^quote s^
+ " against any allowed types.")
end
fun read_pgval ty s = (ty, read_pguval ty s)
-
+
fun pgval_to_string (_, Pgvalnull) = ""
| pgval_to_string (_, Pgvalbool b) = bool_to_pgstring b
| pgval_to_string (_, Pgvalnat n) = int_to_pgstring n
@@ -329,11 +329,11 @@
datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug
type location = { descr: string option,
- url: pgipurl option,
- line: int option,
- column: int option,
- char: int option,
- length: int option }
+ url: pgipurl option,
+ line: int option,
+ column: int option,
+ char: int option,
+ length: int option }
@@ -341,10 +341,10 @@
fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
- case Url.explode url of
+ case Url.explode url of
(Url.File path) => path
- | _ => raise PGIP ("Cannot access non-local URL " ^ quote url)
-
+ | _ => raise PGIP ("Cannot access non-local URL " ^ quote url)
+
fun pgipurl_of_path p = p
fun path_of_pgipurl p = p (* potentially raises PGIP, but not with this implementation *)
@@ -385,51 +385,51 @@
fun attrs_of_location ({ descr, url, line, column, char, length }:location) =
let
- val descr = opt_attr "location_descr" descr
- val url = opt_attr_map attrval_of_pgipurl "location_url" url
- val line = opt_attr_map int_to_pgstring "locationline" line
- val column = opt_attr_map int_to_pgstring "locationcolumn" column
- val char = opt_attr_map int_to_pgstring "locationcharacter" char
- val length = opt_attr_map int_to_pgstring "locationlength" length
+ val descr = opt_attr "location_descr" descr
+ val url = opt_attr_map attrval_of_pgipurl "location_url" url
+ val line = opt_attr_map int_to_pgstring "locationline" line
+ val column = opt_attr_map int_to_pgstring "locationcolumn" column
+ val char = opt_attr_map int_to_pgstring "locationcharacter" char
+ val length = opt_attr_map int_to_pgstring "locationlength" length
in
- descr @ url @ line @ column @ char @ length
+ descr @ url @ line @ column @ char @ length
end
fun pgipint_of_string err s =
- case Int.fromString s of
- SOME i => i
- | NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.")
+ case Int.fromString s of
+ SOME i => i
+ | NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.")
fun location_of_attrs attrs =
let
- val descr = get_attr_opt "location_descr" attrs
- val url = Option.map pgipurl_of_string (get_attr_opt "location_url" attrs)
- val line = Option.map (pgipint_of_string "location element line attribute")
- (get_attr_opt "locationline" attrs)
- val column = Option.map (pgipint_of_string "location element column attribute")
- (get_attr_opt "locationcolumn" attrs)
- val char = Option.map (pgipint_of_string "location element char attribute")
- (get_attr_opt "locationcharacter" attrs)
- val length = Option.map (pgipint_of_string "location element length attribute")
- (get_attr_opt "locationlength" attrs)
+ val descr = get_attr_opt "location_descr" attrs
+ val url = Option.map pgipurl_of_string (get_attr_opt "location_url" attrs)
+ val line = Option.map (pgipint_of_string "location element line attribute")
+ (get_attr_opt "locationline" attrs)
+ val column = Option.map (pgipint_of_string "location element column attribute")
+ (get_attr_opt "locationcolumn" attrs)
+ val char = Option.map (pgipint_of_string "location element char attribute")
+ (get_attr_opt "locationcharacter" attrs)
+ val length = Option.map (pgipint_of_string "location element length attribute")
+ (get_attr_opt "locationlength" attrs)
in
- {descr=descr, url=url, line=line, column=column, char=char, length=length}
+ {descr=descr, url=url, line=line, column=column, char=char, length=length}
end
end
(** Preferences **)
type preference = { name: string,
- descr: string option,
- default: string option,
- pgiptype: pgiptype }
+ descr: string option,
+ default: string option,
+ pgiptype: pgiptype }
fun haspref ({ name, descr, default, pgiptype}:preference) =
XML.Elem ("haspref",
- attr "name" name @
- opt_attr "descr" descr @
- opt_attr "default" default,
- [pgiptype_to_xml pgiptype])
+ attr "name" name @
+ opt_attr "descr" descr @
+ opt_attr "default" default,
+ [pgiptype_to_xml pgiptype])
end
diff -r 359764333bf4 -r 1ff5167592ba src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML Wed Aug 27 12:00:28 2008 +0200
@@ -18,29 +18,29 @@
datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
datatype pgmlaction = Toggle | Button | Menu
-
+
datatype pgmlterm =
- Atoms of { kind: string option, content: pgmlatom list }
- | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
- | Break of { mandatory: bool option, indent: int option }
- | Subterm of { kind: string option,
- param: string option,
- place: pgmlplace option,
- name: string option,
- decoration: pgmldec option,
- action: pgmlaction option,
- pos: string option,
- xref: PgipTypes.pgipurl option,
- content: pgmlterm list }
- | Alt of { kind: string option, content: pgmlterm list }
- | Embed of XML.tree list
- | Raw of XML.tree
+ Atoms of { kind: string option, content: pgmlatom list }
+ | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
+ | Break of { mandatory: bool option, indent: int option }
+ | Subterm of { kind: string option,
+ param: string option,
+ place: pgmlplace option,
+ name: string option,
+ decoration: pgmldec option,
+ action: pgmlaction option,
+ pos: string option,
+ xref: PgipTypes.pgipurl option,
+ content: pgmlterm list }
+ | Alt of { kind: string option, content: pgmlterm list }
+ | Embed of XML.tree list
+ | Raw of XML.tree
datatype pgml =
- Pgml of { version: string option, systemid: string option,
- area: PgipTypes.displayarea option,
- content: pgmlterm list }
-
+ Pgml of { version: string option, systemid: string option,
+ area: PgipTypes.displayarea option,
+ content: pgmlterm list }
+
val pgmlterm_to_xml : pgmlterm -> XML.tree
val pgml_to_xml : pgml -> XML.tree
@@ -62,29 +62,29 @@
datatype pgmldec = Bold | Italic | Error | Warning | Info | Other of string
datatype pgmlaction = Toggle | Button | Menu
-
+
datatype pgmlterm =
- Atoms of { kind: string option, content: pgmlatom list }
- | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
- | Break of { mandatory: bool option, indent: int option }
- | Subterm of { kind: string option,
- param: string option,
- place: pgmlplace option,
- name: string option,
- decoration: pgmldec option,
- action: pgmlaction option,
- pos: string option,
- xref: PgipTypes.pgipurl option,
- content: pgmlterm list }
- | Alt of { kind: string option, content: pgmlterm list }
- | Embed of XML.tree list
- | Raw of XML.tree
+ Atoms of { kind: string option, content: pgmlatom list }
+ | Box of { orient: pgmlorient option, indent: int option, content: pgmlterm list }
+ | Break of { mandatory: bool option, indent: int option }
+ | Subterm of { kind: string option,
+ param: string option,
+ place: pgmlplace option,
+ name: string option,
+ decoration: pgmldec option,
+ action: pgmlaction option,
+ pos: string option,
+ xref: PgipTypes.pgipurl option,
+ content: pgmlterm list }
+ | Alt of { kind: string option, content: pgmlterm list }
+ | Embed of XML.tree list
+ | Raw of XML.tree
-
+
datatype pgml =
- Pgml of { version: string option, systemid: string option,
- area: PgipTypes.displayarea option,
- content: pgmlterm list }
+ Pgml of { version: string option, systemid: string option,
+ area: PgipTypes.displayarea option,
+ content: pgmlterm list }
fun pgmlorient_to_string HOVOrient = "hov"
| pgmlorient_to_string HOrient = "h"
@@ -111,35 +111,35 @@
would be better not to *)
fun atom_to_xml (Sym {name,content}) = XML.Elem("sym",attr name name,[XML.Output content])
| atom_to_xml (Str str) = XML.Output str
-
+
fun pgmlterm_to_xml (Atoms {kind, content}) =
- XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
+ XML.Elem("atom",opt_attr "kind" kind, map atom_to_xml content)
| pgmlterm_to_xml (Box {orient, indent, content}) =
- XML.Elem("box",
- opt_attr_map pgmlorient_to_string "orient" orient @
- opt_attr_map int_to_pgstring "indent" indent,
- map pgmlterm_to_xml content)
+ XML.Elem("box",
+ opt_attr_map pgmlorient_to_string "orient" orient @
+ opt_attr_map int_to_pgstring "indent" indent,
+ map pgmlterm_to_xml content)
| pgmlterm_to_xml (Break {mandatory, indent}) =
- XML.Elem("break",
- opt_attr_map bool_to_pgstring "mandatory" mandatory @
- opt_attr_map int_to_pgstring "indent" indent, [])
+ XML.Elem("break",
+ opt_attr_map bool_to_pgstring "mandatory" mandatory @
+ opt_attr_map int_to_pgstring "indent" indent, [])
| pgmlterm_to_xml (Subterm {kind, param, place, name, decoration, action, pos, xref, content}) =
- XML.Elem("subterm",
- opt_attr "kind" kind @
- opt_attr "param" param @
- opt_attr_map pgmlplace_to_string "place" place @
- opt_attr "name" name @
- opt_attr_map pgmldec_to_string "decoration" decoration @
- opt_attr_map pgmlaction_to_string "action" action @
- opt_attr "pos" pos @
- opt_attr_map string_of_pgipurl "xref" xref,
- map pgmlterm_to_xml content)
+ XML.Elem("subterm",
+ opt_attr "kind" kind @
+ opt_attr "param" param @
+ opt_attr_map pgmlplace_to_string "place" place @
+ opt_attr "name" name @
+ opt_attr_map pgmldec_to_string "decoration" decoration @
+ opt_attr_map pgmlaction_to_string "action" action @
+ opt_attr "pos" pos @
+ opt_attr_map string_of_pgipurl "xref" xref,
+ map pgmlterm_to_xml content)
| pgmlterm_to_xml (Alt {kind, content}) =
- XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
+ XML.Elem("alt", opt_attr "kind" kind, map pgmlterm_to_xml content)
| pgmlterm_to_xml (Embed xmls) = XML.Elem("embed", [], xmls)
@@ -147,14 +147,14 @@
datatype pgml =
- Pgml of { version: string option, systemid: string option,
- area: PgipTypes.displayarea option,
- content: pgmlterm list }
+ Pgml of { version: string option, systemid: string option,
+ area: PgipTypes.displayarea option,
+ content: pgmlterm list }
fun pgml_to_xml (Pgml {version,systemid,area,content}) =
- XML.Elem("pgml",
- opt_attr "version" version @
- opt_attr "systemid" systemid @
- Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
- map pgmlterm_to_xml content)
+ XML.Elem("pgml",
+ opt_attr "version" version @
+ opt_attr "systemid" systemid @
+ Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
+ map pgmlterm_to_xml content)
end
diff -r 359764333bf4 -r 1ff5167592ba src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Aug 27 12:00:28 2008 +0200
@@ -178,7 +178,7 @@
let
val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
val deps = Symtab.keys (fold Proofterm.thms_of_proof'
- (map Thm.proof_of ths) Symtab.empty);
+ (map Thm.proof_of ths) Symtab.empty);
in
if null names orelse null deps then ()
else thm_deps_message (spaces_quote names, spaces_quote deps)
diff -r 359764333bf4 -r 1ff5167592ba src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Wed Aug 27 12:00:28 2008 +0200
@@ -763,7 +763,7 @@
val location = #location vs (* TODO: extract position *)
val _ = start_delay_msgs () (* gather parsing errs/warns *)
- val doc = PgipParser.pgip_parser Position.none text
+ val doc = PgipParser.pgip_parser Position.none text
val errs = end_delayed_msgs ()
val sysattrs = PgipTypes.opt_attr "systemdata" systemdata