HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed Jul 20 10:11:08 2011 +0200 (2011-07-20)
changeset 439186ca79a354c51
parent 43917 bce3de79c8ce
child 43925 f651cb053927
HOL/Import reorganization/cleaning. Factor 9 speedup. Remove Import XML parser in favor of much faster of Isabelle's XML parser. Remove ImportRecording since we can use Isabelle images.
src/HOL/Import/HOL4Setup.thy
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Import/ImportRecorder.thy
src/HOL/Import/import_syntax.ML
src/HOL/Import/importrecorder.ML
src/HOL/Import/lazy_seq.ML
src/HOL/Import/mono_scan.ML
src/HOL/Import/mono_seq.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Import/scan.ML
src/HOL/Import/seq.ML
src/HOL/Import/xml.ML
src/HOL/Import/xmlconv.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Import/HOL4Setup.thy	Wed Jul 20 08:46:17 2011 +0200
     1.2 +++ b/src/HOL/Import/HOL4Setup.thy	Wed Jul 20 10:11:08 2011 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Sebastian Skalberg (TU Muenchen)
     1.5  *)
     1.6  
     1.7 -theory HOL4Setup imports MakeEqual ImportRecorder
     1.8 +theory HOL4Setup imports MakeEqual
     1.9    uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import.ML") begin
    1.10  
    1.11  section {* General Setup *}
     2.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Wed Jul 20 08:46:17 2011 +0200
     2.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Wed Jul 20 10:11:08 2011 +0200
     2.3 @@ -1273,9 +1273,9 @@
     2.4    "NSUM_ADD_GEN" > "HOLLight.hollight.NSUM_ADD_GEN"
     2.5    "NSUM_ADD" > "HOLLight.hollight.NSUM_ADD"
     2.6    "NSUM_0" > "HOLLight.hollight.NSUM_0"
     2.7 -  "NOT_UNIV_PSUBSET" > "Complete_Lattice.complete_lattice_class.not_top_less"
     2.8 +  "NOT_UNIV_PSUBSET" > "Orderings.top_class.not_top_less"
     2.9    "NOT_SUC" > "Nat.Suc_not_Zero"
    2.10 -  "NOT_PSUBSET_EMPTY" > "Complete_Lattice.complete_lattice_class.not_less_bot"
    2.11 +  "NOT_PSUBSET_EMPTY" > "Orderings.bot_class.not_less_bot"
    2.12    "NOT_ODD" > "HOLLight.hollight.NOT_ODD"
    2.13    "NOT_LT" > "Orderings.linorder_class.not_less"
    2.14    "NOT_LE" > "Orderings.linorder_class.not_le"
    2.15 @@ -1644,7 +1644,7 @@
    2.16    "IMAGE_INJECTIVE_IMAGE_OF_SUBSET" > "HOLLight.hollight.IMAGE_INJECTIVE_IMAGE_OF_SUBSET"
    2.17    "IMAGE_IMP_INJECTIVE_GEN" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE_GEN"
    2.18    "IMAGE_IMP_INJECTIVE" > "HOLLight.hollight.IMAGE_IMP_INJECTIVE"
    2.19 -  "IMAGE_ID" > "Fun.image_ident"
    2.20 +  "IMAGE_ID" > "Set.image_ident"
    2.21    "IMAGE_I" > "Fun.image_id"
    2.22    "IMAGE_EQ_EMPTY" > "Set.image_is_empty"
    2.23    "IMAGE_DIFF_INJ" > "HOLLight.hollight.IMAGE_DIFF_INJ"
     3.1 --- a/src/HOL/Import/ImportRecorder.thy	Wed Jul 20 08:46:17 2011 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,4 +0,0 @@
     3.4 -theory ImportRecorder imports Main 
     3.5 -uses  "seq.ML" "scan.ML" "mono_seq.ML" "mono_scan.ML" "lazy_seq.ML" "xml.ML" "xmlconv.ML" "importrecorder.ML"
     3.6 -begin
     3.7 -end
     3.8 \ No newline at end of file
     4.1 --- a/src/HOL/Import/import_syntax.ML	Wed Jul 20 08:46:17 2011 +0200
     4.2 +++ b/src/HOL/Import/import_syntax.ML	Wed Jul 20 10:11:08 2011 +0200
     4.3 @@ -19,9 +19,6 @@
     4.4      val const_moves   : (theory -> theory) parser
     4.5      val const_renames : (theory -> theory) parser
     4.6  
     4.7 -    val skip_import_dir : (theory -> theory) parser
     4.8 -    val skip_import     : (theory -> theory) parser
     4.9 -
    4.10      val setup        : unit -> unit
    4.11  end
    4.12  
    4.13 @@ -39,13 +36,6 @@
    4.14                                        |> Sign.add_path thyname
    4.15                                        |> add_dump (";setup_theory " ^ thyname))
    4.16  
    4.17 -fun do_skip_import_dir s = (ImportRecorder.set_skip_import_dir (SOME s); I: theory -> theory)
    4.18 -val skip_import_dir = Parse.string >> do_skip_import_dir
    4.19 -
    4.20 -val lower = String.map Char.toLower
    4.21 -fun do_skip_import s = (ImportRecorder.set_skip_import (case lower s of "on" => true | "off" => false | _ => Scan.fail ()); I: theory -> theory)
    4.22 -val skip_import = Parse.short_ident >> do_skip_import
    4.23 -
    4.24  fun end_import toks =
    4.25      Scan.succeed
    4.26          (fn thy =>
    4.27 @@ -54,16 +44,7 @@
    4.28                  val segname = get_import_segment thy
    4.29                  val (int_thms,facts) = Replay.setup_int_thms thyname thy
    4.30                  val thmnames = filter_out (should_ignore thyname thy) facts
    4.31 -                fun replay thy = 
    4.32 -                    let
    4.33 -                        val _ = ImportRecorder.load_history thyname
    4.34 -                        val thy = Replay.import_thms thyname int_thms thmnames thy
    4.35 -                            (*handle x => (ImportRecorder.save_history thyname; raise x)*)  (* FIXME avoid handle x ?? *)
    4.36 -                        val _ = ImportRecorder.save_history thyname
    4.37 -                        val _ = ImportRecorder.clear_history ()
    4.38 -                    in
    4.39 -                        thy
    4.40 -                    end                                 
    4.41 +                fun replay thy = Replay.import_thms thyname int_thms thmnames thy
    4.42              in
    4.43                  thy |> clear_import_thy
    4.44                      |> set_segment thyname segname
    4.45 @@ -225,12 +206,6 @@
    4.46     Outer_Syntax.command "end_import"
    4.47                         "End HOL4 import"
    4.48                         Keyword.thy_decl (end_import >> Toplevel.theory);
    4.49 -   Outer_Syntax.command "skip_import_dir" 
    4.50 -                       "Sets caching directory for skipping importing"
    4.51 -                       Keyword.thy_decl (skip_import_dir >> Toplevel.theory);
    4.52 -   Outer_Syntax.command "skip_import" 
    4.53 -                       "Switches skipping importing on or off"
    4.54 -                       Keyword.thy_decl (skip_import >> Toplevel.theory);                   
    4.55     Outer_Syntax.command "setup_theory"
    4.56                         "Setup HOL4 theory replaying"
    4.57                         Keyword.thy_decl (setup_theory >> Toplevel.theory);
     5.1 --- a/src/HOL/Import/importrecorder.ML	Wed Jul 20 08:46:17 2011 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,265 +0,0 @@
     5.4 -signature IMPORT_RECORDER =
     5.5 -sig
     5.6 -
     5.7 -    datatype deltastate = Consts of (string * typ * mixfix) list
     5.8 -                        | Specification of (string * string * bool) list * term
     5.9 -                        | Hol_mapping of string * string * string
    5.10 -                        | Hol_pending of string * string * term
    5.11 -                        | Hol_const_mapping of string * string * string
    5.12 -                        | Hol_move of string * string
    5.13 -                        | Defs of string * term
    5.14 -                        | Hol_theorem of string * string * term
    5.15 -                        | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
    5.16 -                        | Hol_type_mapping of string * string * string
    5.17 -                        | Indexed_theorem of int * term
    5.18 -                        | Protect_varname of string * string
    5.19 -                        | Dump of string
    5.20 -
    5.21 -    datatype history = History of history_entry list
    5.22 -         and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
    5.23 -
    5.24 -    val get_history : unit -> history
    5.25 -    val set_history : history -> unit
    5.26 -    val clear_history : unit -> unit
    5.27 -                                      
    5.28 -    val start_replay_proof : string -> string -> unit
    5.29 -    val stop_replay_proof : string -> string -> unit
    5.30 -    val abort_replay_proof : string -> string -> unit
    5.31 -
    5.32 -    val add_consts : (string * typ * mixfix) list -> unit
    5.33 -    val add_specification : (string * string * bool) list -> thm -> unit
    5.34 -    val add_hol_mapping : string -> string -> string -> unit
    5.35 -    val add_hol_pending : string -> string -> thm -> unit
    5.36 -    val add_hol_const_mapping : string -> string -> string -> unit
    5.37 -    val add_hol_move : string -> string -> unit
    5.38 -    val add_defs : string -> term -> unit
    5.39 -    val add_hol_theorem : string -> string -> thm -> unit
    5.40 -    val add_typedef :  string option -> string * string list * mixfix -> term -> (string * string) option -> thm -> unit
    5.41 -    val add_hol_type_mapping : string -> string -> string -> unit
    5.42 -    val add_indexed_theorem : int -> thm -> unit
    5.43 -    val protect_varname : string -> string -> unit
    5.44 -    val add_dump : string -> unit
    5.45 -
    5.46 -    val set_skip_import_dir : string option -> unit
    5.47 -    val get_skip_import_dir : unit -> string option
    5.48 -
    5.49 -    val set_skip_import : bool -> unit
    5.50 -    val get_skip_import : unit -> bool
    5.51 -
    5.52 -    val save_history : string -> unit
    5.53 -    val load_history : string -> unit
    5.54 -end
    5.55 -
    5.56 -structure ImportRecorder :> IMPORT_RECORDER  =
    5.57 -struct
    5.58 -
    5.59 -datatype deltastate = Consts of (string * typ * mixfix) list
    5.60 -                    | Specification of (string * string * bool) list * term
    5.61 -                    | Hol_mapping of string * string * string
    5.62 -                    | Hol_pending of string * string * term
    5.63 -                    | Hol_const_mapping of string * string * string
    5.64 -                    | Hol_move of string * string
    5.65 -                    | Defs of string * term
    5.66 -                    | Hol_theorem of string * string * term
    5.67 -                    | Typedef of string option * (string * string list * mixfix) * term * (string * string) option * term 
    5.68 -                    | Hol_type_mapping of string * string * string
    5.69 -                    | Indexed_theorem of int * term
    5.70 -                    | Protect_varname of string * string
    5.71 -                    | Dump of string
    5.72 -
    5.73 -datatype history_entry = StartReplay of string*string  
    5.74 -                       | StopReplay of string*string
    5.75 -                       | AbortReplay of string*string
    5.76 -                       | Delta of deltastate list
    5.77 -
    5.78 -val history = Unsynchronized.ref ([]:history_entry list)
    5.79 -val history_dir = Unsynchronized.ref (SOME "")
    5.80 -val skip_imports = Unsynchronized.ref false
    5.81 -
    5.82 -fun set_skip_import b = skip_imports := b
    5.83 -fun get_skip_import () = !skip_imports
    5.84 -
    5.85 -fun clear_history () = history := []
    5.86 -
    5.87 -fun add_delta d = history := (case !history of (Delta ds)::hs => (Delta (d::ds))::hs | hs => (Delta [d])::hs)
    5.88 -fun add_replay r = history := (r :: (!history))
    5.89 -
    5.90 -local 
    5.91 -    open XMLConvOutput
    5.92 -    val consts = list (triple string typ mixfix)
    5.93 -    val specification = pair (list (triple string string bool)) term
    5.94 -    val hol_mapping = triple string string string
    5.95 -    val hol_pending = triple string string term
    5.96 -    val hol_const_mapping = triple string string string
    5.97 -    val hol_move = pair string string
    5.98 -    val defs = pair string term
    5.99 -    val hol_theorem = triple string string term
   5.100 -    val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
   5.101 -    val hol_type_mapping = triple string string string
   5.102 -    val indexed_theorem = pair int term
   5.103 -    val entry = pair string string
   5.104 -
   5.105 -    fun delta (Consts args) = wrap "consts" consts args
   5.106 -      | delta (Specification args) = wrap "specification" specification args
   5.107 -      | delta (Hol_mapping args) = wrap "hol_mapping" hol_mapping args
   5.108 -      | delta (Hol_pending args) = wrap "hol_pending" hol_pending args
   5.109 -      | delta (Hol_const_mapping args) = wrap "hol_const_mapping" hol_const_mapping args
   5.110 -      | delta (Hol_move args) = wrap "hol_move" hol_move args
   5.111 -      | delta (Defs args) = wrap "defs" defs args
   5.112 -      | delta (Hol_theorem args) = wrap "hol_theorem" hol_theorem args
   5.113 -      | delta (Typedef args) = wrap "typedef" typedef args
   5.114 -      | delta (Hol_type_mapping args) = wrap "hol_type_mapping" hol_type_mapping args
   5.115 -      | delta (Indexed_theorem args) = wrap "indexed_theorem" indexed_theorem args
   5.116 -      | delta (Protect_varname args) = wrap "protect_varname" entry args
   5.117 -      | delta (Dump args) = wrap "dump" string args
   5.118 -
   5.119 -    fun history_entry (StartReplay args) = wrap "startreplay" entry args
   5.120 -      | history_entry (StopReplay args) = wrap "stopreplay" entry args
   5.121 -      | history_entry (AbortReplay args) = wrap "abortreplay" entry args
   5.122 -      | history_entry (Delta args) = wrap "delta" (list delta) args
   5.123 -in
   5.124 -
   5.125 -val xml_of_history = list history_entry
   5.126 -
   5.127 -end
   5.128 -
   5.129 -local 
   5.130 -    open XMLConvInput
   5.131 -    val consts = list (triple string typ mixfix)
   5.132 -    val specification = pair (list (triple string string bool)) term
   5.133 -    val hol_mapping = triple string string string
   5.134 -    val hol_pending = triple string string term
   5.135 -    val hol_const_mapping = triple string string string
   5.136 -    val hol_move = pair string string
   5.137 -    val defs = pair string term
   5.138 -    val hol_theorem = triple string string term
   5.139 -    val typedef = quintuple (option string) (triple string (list string) mixfix) term (option (pair string string)) term
   5.140 -    val hol_type_mapping = triple string string string
   5.141 -    val indexed_theorem = pair int term
   5.142 -    val entry = pair string string
   5.143 -
   5.144 -    fun delta "consts" = unwrap Consts consts
   5.145 -      | delta "specification" = unwrap Specification specification 
   5.146 -      | delta "hol_mapping" = unwrap Hol_mapping hol_mapping 
   5.147 -      | delta "hol_pending" = unwrap Hol_pending hol_pending
   5.148 -      | delta "hol_const_mapping" = unwrap Hol_const_mapping hol_const_mapping
   5.149 -      | delta "hol_move" = unwrap Hol_move hol_move
   5.150 -      | delta "defs" = unwrap Defs defs
   5.151 -      | delta "hol_theorem" = unwrap Hol_theorem hol_theorem
   5.152 -      | delta "typedef" = unwrap Typedef typedef
   5.153 -      | delta "hol_type_mapping" = unwrap Hol_type_mapping hol_type_mapping
   5.154 -      | delta "indexed_theorem" = unwrap Indexed_theorem indexed_theorem
   5.155 -      | delta "protect_varname" = unwrap Protect_varname entry
   5.156 -      | delta "dump" = unwrap Dump string
   5.157 -      | delta _ = raise ParseException "delta"
   5.158 -
   5.159 -    val delta = fn e => delta (name_of_wrap e) e
   5.160 -
   5.161 -    fun history_entry "startreplay" = unwrap StartReplay entry 
   5.162 -      | history_entry "stopreplay" = unwrap StopReplay entry
   5.163 -      | history_entry "abortreplay" = unwrap AbortReplay entry
   5.164 -      | history_entry "delta" = unwrap Delta (list delta)
   5.165 -      | history_entry _ = raise ParseException "history_entry"
   5.166 -
   5.167 -    val history_entry = fn e => history_entry (name_of_wrap e) e
   5.168 -in
   5.169 -
   5.170 -val history_of_xml = list history_entry
   5.171 -
   5.172 -end
   5.173 -
   5.174 -fun start_replay_proof thyname thmname = add_replay (StartReplay (thyname, thmname))
   5.175 -fun stop_replay_proof thyname thmname = add_replay (StopReplay (thyname, thmname))
   5.176 -fun abort_replay_proof thyname thmname = add_replay (AbortReplay (thyname, thmname))
   5.177 -fun add_hol_theorem thyname thmname thm = add_delta (Hol_theorem (thyname, thmname, prop_of thm))
   5.178 -fun add_hol_mapping thyname thmname isaname = add_delta (Hol_mapping (thyname, thmname, isaname))
   5.179 -fun add_consts consts = add_delta (Consts consts)
   5.180 -fun add_typedef thmname_opt typ c absrep_opt th = add_delta (Typedef (thmname_opt, typ, c, absrep_opt, prop_of th))
   5.181 -fun add_defs thmname eq = add_delta (Defs (thmname, eq)) 
   5.182 -fun add_hol_const_mapping thyname constname fullcname = add_delta (Hol_const_mapping (thyname, constname, fullcname))
   5.183 -fun add_hol_move fullname moved_thmname = add_delta (Hol_move (fullname, moved_thmname))
   5.184 -fun add_hol_type_mapping thyname tycname fulltyname = add_delta (Hol_type_mapping (thyname, tycname, fulltyname))
   5.185 -fun add_hol_pending thyname thmname th = add_delta (Hol_pending (thyname, thmname, prop_of th))
   5.186 -fun add_specification names th = add_delta (Specification (names, prop_of th)) 
   5.187 -fun add_indexed_theorem i th = add_delta (Indexed_theorem (i, prop_of th))
   5.188 -fun protect_varname s t = add_delta (Protect_varname (s,t))
   5.189 -fun add_dump s = add_delta (Dump s)
   5.190 -                            
   5.191 -fun set_skip_import_dir dir = (history_dir := dir)
   5.192 -fun get_skip_import_dir () = !history_dir
   5.193 -
   5.194 -fun get_filename thyname = Path.implode (Path.append (Path.explode (the (get_skip_import_dir ()))) (Path.explode (thyname^".history")))
   5.195 -
   5.196 -fun save_history thyname = 
   5.197 -    if get_skip_import () then
   5.198 -        XMLConv.write_to_file xml_of_history (get_filename thyname) (!history)
   5.199 -    else 
   5.200 -        ()
   5.201 -
   5.202 -fun load_history thyname = 
   5.203 -    if get_skip_import () then
   5.204 -        let 
   5.205 -            val filename = get_filename thyname
   5.206 -            val _ = writeln "load_history / before"
   5.207 -            val _ = 
   5.208 -                if File.exists (Path.explode filename) then                                     
   5.209 -                    (history := XMLConv.read_from_file history_of_xml (get_filename thyname)) 
   5.210 -                else
   5.211 -                    clear_history ()
   5.212 -            val _ = writeln "load_history / after"
   5.213 -        in
   5.214 -            ()
   5.215 -        end
   5.216 -    else
   5.217 -        ()
   5.218 -    
   5.219 - 
   5.220 -datatype history = History of history_entry list
   5.221 -     and history_entry = ThmEntry of string*string*bool*history | DeltaEntry of deltastate list
   5.222 -
   5.223 -exception CONV 
   5.224 -
   5.225 -fun conv_histories ((StartReplay (thyname, thmname))::rest) = 
   5.226 -    let
   5.227 -        val (hs, rest) = conv_histories rest
   5.228 -        fun continue thyname' thmname' aborted rest = 
   5.229 -            if thyname = thyname' andalso thmname = thmname' then
   5.230 -                let
   5.231 -                    val (hs', rest) = conv_histories rest
   5.232 -                in
   5.233 -                    ((ThmEntry (thyname, thmname, aborted, History hs))::hs', rest)
   5.234 -                end
   5.235 -            else
   5.236 -                raise CONV 
   5.237 -    in
   5.238 -        case rest of 
   5.239 -            (StopReplay (thyname',thmname'))::rest =>
   5.240 -            continue thyname' thmname' false rest
   5.241 -          | (AbortReplay (thyname',thmname'))::rest =>
   5.242 -            continue thyname' thmname' true rest
   5.243 -          | [] => (hs, [])
   5.244 -          | _ => raise CONV
   5.245 -    end
   5.246 -  | conv_histories ((Delta ds)::rest) = (conv_histories rest) |>> (fn hs => (DeltaEntry (rev ds))::hs)  
   5.247 -  | conv_histories rest = ([], rest)
   5.248 -
   5.249 -fun conv es = 
   5.250 -    let
   5.251 -        val (h, rest) = conv_histories (rev es)
   5.252 -    in
   5.253 -        case rest of
   5.254 -            [] => h
   5.255 -          | _ => raise CONV
   5.256 -    end 
   5.257 -
   5.258 -fun get_history () = History (conv (!history))
   5.259 -
   5.260 -fun reconv (History hs) rs = fold reconv_entry hs rs
   5.261 -and reconv_entry (ThmEntry (thyname, thmname, aborted, h)) rs =
   5.262 -    ((if aborted then AbortReplay else StopReplay) (thyname, thmname)) :: (reconv h ((StartReplay (thyname, thmname))::rs))
   5.263 -  | reconv_entry (DeltaEntry ds) rs = (Delta (rev ds))::rs
   5.264 -    
   5.265 -fun set_history h = history := reconv h []
   5.266 -
   5.267 -
   5.268 -end
     6.1 --- a/src/HOL/Import/lazy_seq.ML	Wed Jul 20 08:46:17 2011 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,551 +0,0 @@
     6.4 -(*  Title:      HOL/Import/lazy_seq.ML
     6.5 -    Author:     Sebastian Skalberg, TU Muenchen
     6.6 -
     6.7 -Alternative version of lazy sequences.
     6.8 -*)
     6.9 -
    6.10 -signature LAZY_SEQ =
    6.11 -sig
    6.12 -
    6.13 -    include EXTENDED_SCANNER_SEQ
    6.14 -
    6.15 -    (* From LIST *)
    6.16 -
    6.17 -    val fromString : string -> string seq
    6.18 -    val @ : 'a seq * 'a seq -> 'a seq
    6.19 -    val hd : 'a seq -> 'a
    6.20 -    val tl : 'a seq -> 'a seq
    6.21 -    val last : 'a seq -> 'a
    6.22 -    val getItem : 'a seq -> ('a * 'a seq) option
    6.23 -    val nth : 'a seq * int -> 'a
    6.24 -    val take : 'a seq * int -> 'a seq
    6.25 -    val drop : 'a seq * int -> 'a seq
    6.26 -    val rev : 'a seq -> 'a seq
    6.27 -    val concat : 'a seq seq -> 'a seq
    6.28 -    val revAppend : 'a seq * 'a seq -> 'a seq
    6.29 -    val app : ('a -> unit) -> 'a seq -> unit
    6.30 -    val map : ('a -> 'b) -> 'a seq -> 'b seq
    6.31 -    val mapPartial : ('a -> 'b option) -> 'a seq -> 'b seq
    6.32 -    val find : ('a -> bool) -> 'a seq -> 'a option
    6.33 -    val filter : ('a -> bool) -> 'a seq -> 'a seq
    6.34 -    val partition : ('a -> bool)
    6.35 -                      -> 'a seq -> 'a seq * 'a seq
    6.36 -    val foldl : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
    6.37 -    val foldr : ('a * 'b -> 'b) -> 'b -> 'a seq -> 'b
    6.38 -    val exists : ('a -> bool) -> 'a seq -> bool
    6.39 -    val all : ('a -> bool) -> 'a seq -> bool
    6.40 -    val tabulate : int * (int -> 'a) -> 'a seq
    6.41 -    val collate : ('a * 'a -> order)
    6.42 -                    -> 'a seq * 'a seq -> order 
    6.43 -
    6.44 -    (* Miscellaneous *)
    6.45 -
    6.46 -    val cycle      : ((unit ->'a seq) -> 'a seq) -> 'a seq
    6.47 -    val iterates   : ('a -> 'a) -> 'a -> 'a seq
    6.48 -    val of_function: (unit -> 'a option) -> 'a seq
    6.49 -    val of_string  : string -> char seq
    6.50 -    val of_instream: TextIO.instream -> char seq
    6.51 -
    6.52 -    (* From SEQ *)
    6.53 -
    6.54 -    val make: (unit -> ('a * 'a seq) option) -> 'a seq
    6.55 -    val empty: 'a -> 'a seq
    6.56 -    val cons: 'a * 'a seq -> 'a seq
    6.57 -    val single: 'a -> 'a seq
    6.58 -    val try: ('a -> 'b) -> 'a -> 'b seq
    6.59 -    val chop: int * 'a seq -> 'a list * 'a seq
    6.60 -    val list_of: 'a seq -> 'a list
    6.61 -    val of_list: 'a list -> 'a seq
    6.62 -    val mapp: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    6.63 -    val interleave: 'a seq * 'a seq -> 'a seq
    6.64 -    val print: (int -> 'a -> unit) -> int -> 'a seq -> unit
    6.65 -    val it_right : ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    6.66 -    val commute: 'a seq list -> 'a list seq
    6.67 -    val succeed: 'a -> 'a seq
    6.68 -    val fail: 'a -> 'b seq
    6.69 -    val THEN: ('a -> 'b seq) * ('b -> 'c seq) -> 'a -> 'c seq
    6.70 -    val ORELSE: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    6.71 -    val APPEND: ('a -> 'b seq) * ('a -> 'b seq) -> 'a -> 'b seq
    6.72 -    val EVERY: ('a -> 'a seq) list -> 'a -> 'a seq
    6.73 -    val FIRST: ('a -> 'b seq) list -> 'a -> 'b seq
    6.74 -    val TRY: ('a -> 'a seq) -> 'a -> 'a seq
    6.75 -    val REPEAT: ('a -> 'a seq) -> 'a -> 'a seq
    6.76 -    val REPEAT1: ('a -> 'a seq) -> 'a -> 'a seq
    6.77 -    val INTERVAL: (int -> 'a -> 'a seq) -> int -> int -> 'a -> 'a seq
    6.78 -    val DETERM: ('a -> 'b seq) -> 'a -> 'b seq
    6.79 -
    6.80 -end
    6.81 -
    6.82 -structure LazySeq :> LAZY_SEQ =
    6.83 -struct
    6.84 -
    6.85 -datatype 'a seq = Seq of ('a * 'a seq) option lazy
    6.86 -
    6.87 -exception Empty
    6.88 -
    6.89 -fun getItem (Seq s) = Lazy.force s
    6.90 -val pull = getItem
    6.91 -fun make f = Seq (Lazy.lazy f)
    6.92 -
    6.93 -fun null s = is_none (getItem s)
    6.94 -
    6.95 -local
    6.96 -    fun F n NONE = n
    6.97 -      | F n (SOME(_,s)) = F (n+1) (getItem s)
    6.98 -in
    6.99 -fun length s = F 0 (getItem s)
   6.100 -end
   6.101 -
   6.102 -fun s1 @ s2 =
   6.103 -    let
   6.104 -        fun F NONE = getItem s2
   6.105 -          | F (SOME(x,s1')) = SOME(x,F' s1')
   6.106 -        and F' s = make (fn () => F (getItem s))
   6.107 -    in
   6.108 -        F' s1
   6.109 -    end
   6.110 -
   6.111 -local
   6.112 -    fun F NONE = raise Empty
   6.113 -      | F (SOME arg) = arg
   6.114 -in
   6.115 -fun hd s = #1 (F (getItem s))
   6.116 -fun tl s = #2 (F (getItem s))
   6.117 -end
   6.118 -
   6.119 -local
   6.120 -    fun F x NONE = x
   6.121 -      | F _ (SOME(x,s)) = F x (getItem s)
   6.122 -    fun G NONE = raise Empty
   6.123 -      | G (SOME(x,s)) = F x (getItem s)
   6.124 -in
   6.125 -fun last s = G (getItem s)
   6.126 -end
   6.127 -
   6.128 -local
   6.129 -    fun F NONE _ = raise Subscript
   6.130 -      | F (SOME(x,_)) 0 = x
   6.131 -      | F (SOME(_,s)) n = F (getItem s) (n-1)
   6.132 -in
   6.133 -fun nth(s,n) =
   6.134 -    if n < 0
   6.135 -    then raise Subscript
   6.136 -    else F (getItem s) n
   6.137 -end
   6.138 -
   6.139 -local
   6.140 -    fun F NONE _ = raise Subscript
   6.141 -      | F (SOME(x,s)) n = SOME(x,F' s (n-1))
   6.142 -    and F' s 0 = Seq (Lazy.value NONE)
   6.143 -      | F' s n = make (fn () => F (getItem s) n)
   6.144 -in
   6.145 -fun take (s,n) =
   6.146 -    if n < 0
   6.147 -    then raise Subscript
   6.148 -    else F' s n
   6.149 -end
   6.150 -
   6.151 -fun take_at_most s n = 
   6.152 -    if n <= 0 then [] else
   6.153 -    case getItem s of 
   6.154 -        NONE => []
   6.155 -      | SOME (x,s') => x::(take_at_most s' (n-1))
   6.156 -
   6.157 -local
   6.158 -    fun F s 0 = s
   6.159 -      | F NONE _ = raise Subscript
   6.160 -      | F (SOME(_,s)) n = F (getItem s) (n-1)
   6.161 -in
   6.162 -fun drop (s,0) = s
   6.163 -  | drop (s,n) = 
   6.164 -    if n < 0
   6.165 -    then raise Subscript
   6.166 -    else make (fn () => F (getItem s) n)
   6.167 -end
   6.168 -
   6.169 -local
   6.170 -    fun F s NONE = s
   6.171 -      | F s (SOME(x,s')) = F (SOME(x, Seq (Lazy.value s))) (getItem s')
   6.172 -in
   6.173 -fun rev s = make (fn () => F NONE (getItem s))
   6.174 -end
   6.175 -
   6.176 -local
   6.177 -    fun F s NONE = getItem s
   6.178 -      | F s (SOME(x,s')) = F (Seq (Lazy.value (SOME(x,s)))) (getItem s')
   6.179 -in
   6.180 -fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
   6.181 -end
   6.182 -
   6.183 -local
   6.184 -    fun F NONE = NONE
   6.185 -      | F (SOME(s1,s2)) =
   6.186 -        let
   6.187 -            fun G NONE = F (getItem s2)
   6.188 -              | G (SOME(x,s)) = SOME(x,make (fn () => G (getItem s)))
   6.189 -        in
   6.190 -            G (getItem s1)
   6.191 -        end
   6.192 -in
   6.193 -fun concat s = make (fn () => F (getItem s))
   6.194 -end
   6.195 -
   6.196 -fun app f =
   6.197 -    let
   6.198 -        fun F NONE = ()
   6.199 -          | F (SOME(x,s)) =
   6.200 -            (f x;
   6.201 -             F (getItem s))
   6.202 -    in
   6.203 -        F o getItem
   6.204 -    end
   6.205 -
   6.206 -fun map f =
   6.207 -    let
   6.208 -        fun F NONE = NONE
   6.209 -          | F (SOME(x,s)) = SOME(f x,F' s)
   6.210 -        and F' s = make (fn() => F (getItem s))
   6.211 -    in
   6.212 -        F'
   6.213 -    end
   6.214 -
   6.215 -fun mapPartial f =
   6.216 -    let
   6.217 -        fun F NONE = NONE
   6.218 -          | F (SOME(x,s)) =
   6.219 -            (case f x of
   6.220 -                 SOME y => SOME(y,F' s)
   6.221 -               | NONE => F (getItem s))
   6.222 -        and F' s = make (fn()=> F (getItem s))
   6.223 -    in
   6.224 -        F'
   6.225 -    end
   6.226 -
   6.227 -fun find P =
   6.228 -    let
   6.229 -        fun F NONE = NONE
   6.230 -          | F (SOME(x,s)) =
   6.231 -            if P x
   6.232 -            then SOME x
   6.233 -            else F (getItem s)
   6.234 -    in
   6.235 -        F o getItem
   6.236 -    end
   6.237 -
   6.238 -(*fun filter p = mapPartial (fn x => if p x then SOME x else NONE)*)
   6.239 -
   6.240 -fun filter P =
   6.241 -    let
   6.242 -        fun F NONE = NONE
   6.243 -          | F (SOME(x,s)) =
   6.244 -            if P x
   6.245 -            then SOME(x,F' s)
   6.246 -            else F (getItem s)
   6.247 -        and F' s = make (fn () => F (getItem s))
   6.248 -    in
   6.249 -        F'
   6.250 -    end
   6.251 -
   6.252 -fun partition f s =
   6.253 -    let
   6.254 -        val s' = map (fn x => (x,f x)) s
   6.255 -    in
   6.256 -        (mapPartial (fn (x,true) => SOME x | _ => NONE) s',
   6.257 -         mapPartial (fn (x,false) => SOME x | _ => NONE) s')
   6.258 -    end
   6.259 -
   6.260 -fun exists P =
   6.261 -    let
   6.262 -        fun F NONE = false
   6.263 -          | F (SOME(x,s)) = P x orelse F (getItem s)
   6.264 -    in
   6.265 -        F o getItem
   6.266 -    end
   6.267 -
   6.268 -fun all P =
   6.269 -    let
   6.270 -        fun F NONE = true
   6.271 -          | F (SOME(x,s)) = P x andalso F (getItem s)
   6.272 -    in
   6.273 -        F o getItem
   6.274 -    end
   6.275 -
   6.276 -(*fun tabulate f = map f (iterates (fn x => x + 1) 0)*)
   6.277 -
   6.278 -fun tabulate (n,f) =
   6.279 -    let
   6.280 -        fun F n = make (fn () => SOME(f n,F (n+1)))
   6.281 -    in
   6.282 -        F n
   6.283 -    end
   6.284 -
   6.285 -fun collate c (s1,s2) =
   6.286 -    let
   6.287 -        fun F NONE _ = LESS
   6.288 -          | F _ NONE = GREATER
   6.289 -          | F (SOME(x,s1)) (SOME(y,s2)) =
   6.290 -            (case c (x,y) of
   6.291 -                 LESS => LESS
   6.292 -               | GREATER => GREATER
   6.293 -               | EQUAL => F' s1 s2)
   6.294 -        and F' s1 s2 = F (getItem s1) (getItem s2)
   6.295 -    in
   6.296 -        F' s1 s2
   6.297 -    end
   6.298 -
   6.299 -fun empty  _ = Seq (Lazy.value NONE)
   6.300 -fun single x = Seq(Lazy.value (SOME(x,Seq (Lazy.value NONE))))
   6.301 -fun cons a = Seq(Lazy.value (SOME a))
   6.302 -
   6.303 -fun cycle seqfn =
   6.304 -    let
   6.305 -        val knot = Unsynchronized.ref (Seq (Lazy.value NONE))
   6.306 -    in
   6.307 -        knot := seqfn (fn () => !knot);
   6.308 -        !knot
   6.309 -    end
   6.310 -
   6.311 -fun iterates f =
   6.312 -    let
   6.313 -        fun F x = make (fn() => SOME(x,F (f x)))
   6.314 -    in
   6.315 -        F
   6.316 -    end
   6.317 -
   6.318 -fun interleave (s1,s2) =
   6.319 -    let
   6.320 -        fun F NONE = getItem s2
   6.321 -          | F (SOME(x,s1')) = SOME(x,interleave(s2,s1'))
   6.322 -    in
   6.323 -        make (fn()=> F (getItem s1))
   6.324 -    end
   6.325 -
   6.326 -(* val force_all = app ignore *)
   6.327 -
   6.328 -local
   6.329 -    fun F NONE = ()
   6.330 -      | F (SOME(x,s)) = F (getItem s)
   6.331 -in
   6.332 -fun force_all s = F (getItem s)
   6.333 -end
   6.334 -
   6.335 -fun of_function f =
   6.336 -    let
   6.337 -        fun F () = case f () of
   6.338 -                       SOME x => SOME(x,make F)
   6.339 -                     | NONE => NONE
   6.340 -    in
   6.341 -        make F
   6.342 -    end
   6.343 -
   6.344 -local
   6.345 -    fun F [] = NONE
   6.346 -      | F (x::xs) = SOME(x,F' xs)
   6.347 -    and F' xs = make (fn () => F xs)
   6.348 -in
   6.349 -fun of_list xs = F' xs
   6.350 -end
   6.351 -
   6.352 -val of_string = of_list o String.explode
   6.353 -
   6.354 -fun of_instream is =
   6.355 -    let
   6.356 -        val buffer : char list Unsynchronized.ref = Unsynchronized.ref []
   6.357 -        fun get_input () =
   6.358 -            case !buffer of
   6.359 -                (c::cs) => (buffer:=cs;
   6.360 -                            SOME c)
   6.361 -              | [] => (case String.explode (TextIO.input is) of
   6.362 -                           [] => NONE
   6.363 -                         | (c::cs) => (buffer := cs;
   6.364 -                                       SOME c))
   6.365 -    in
   6.366 -        of_function get_input
   6.367 -    end
   6.368 -
   6.369 -local
   6.370 -    fun F k NONE = k []
   6.371 -      | F k (SOME(x,s)) = F (fn xs => k (x::xs)) (getItem s)
   6.372 -in
   6.373 -fun list_of s = F (fn x => x) (getItem s)
   6.374 -end
   6.375 -
   6.376 -(* Adapted from seq.ML *)
   6.377 -
   6.378 -val succeed = single
   6.379 -fun fail _ = Seq (Lazy.value NONE)
   6.380 -
   6.381 -(* fun op THEN (f, g) x = flat (map g (f x)) *)
   6.382 -
   6.383 -fun op THEN (f, g) =
   6.384 -    let
   6.385 -        fun F NONE = NONE
   6.386 -          | F (SOME(x,xs)) =
   6.387 -            let
   6.388 -                fun G NONE = F (getItem xs)
   6.389 -                  | G (SOME(y,ys)) = SOME(y,make (fn () => G (getItem ys)))
   6.390 -            in
   6.391 -                G (getItem (g x))
   6.392 -            end
   6.393 -    in
   6.394 -        fn x => make (fn () => F (getItem (f x)))
   6.395 -    end
   6.396 -
   6.397 -fun op ORELSE (f, g) x =
   6.398 -    make (fn () =>
   6.399 -             case getItem (f x) of
   6.400 -                 NONE => getItem (g x)
   6.401 -               | some => some)
   6.402 -
   6.403 -fun op APPEND (f, g) x =
   6.404 -    let
   6.405 -        fun copy s =
   6.406 -            case getItem s of
   6.407 -                NONE => getItem (g x)
   6.408 -              | SOME(x,xs) => SOME(x,make (fn () => copy xs))
   6.409 -    in
   6.410 -        make (fn () => copy (f x))
   6.411 -    end
   6.412 -
   6.413 -fun EVERY fs = fold_rev (curry op THEN) fs succeed
   6.414 -fun FIRST fs = fold_rev (curry op ORELSE) fs fail
   6.415 -
   6.416 -fun TRY f x =
   6.417 -    make (fn () =>
   6.418 -             case getItem (f x) of
   6.419 -                 NONE => SOME(x,Seq (Lazy.value NONE))
   6.420 -               | some => some)
   6.421 -
   6.422 -fun REPEAT f =
   6.423 -    let
   6.424 -        fun rep qs x =
   6.425 -            case getItem (f x) of
   6.426 -                NONE => SOME(x, make (fn () => repq qs))
   6.427 -              | SOME (x', q) => rep (q :: qs) x'
   6.428 -        and repq [] = NONE
   6.429 -          | repq (q :: qs) =
   6.430 -            case getItem q of
   6.431 -                NONE => repq qs
   6.432 -              | SOME (x, q) => rep (q :: qs) x
   6.433 -    in
   6.434 -     fn x => make (fn () => rep [] x)
   6.435 -    end
   6.436 -
   6.437 -fun REPEAT1 f = op THEN (f, REPEAT f);
   6.438 -
   6.439 -fun INTERVAL f i =
   6.440 -    let
   6.441 -        fun F j =
   6.442 -            if i > j
   6.443 -            then single
   6.444 -            else op THEN (f j, F (j - 1))
   6.445 -    in F end
   6.446 -
   6.447 -fun DETERM f x =
   6.448 -    make (fn () =>
   6.449 -             case getItem (f x) of
   6.450 -                 NONE => NONE
   6.451 -               | SOME (x', _) => SOME(x',Seq (Lazy.value NONE)))
   6.452 -
   6.453 -(*partial function as procedure*)
   6.454 -fun try f x =
   6.455 -    make (fn () =>
   6.456 -             case Basics.try f x of
   6.457 -                 SOME y => SOME(y,Seq (Lazy.value NONE))
   6.458 -               | NONE => NONE)
   6.459 -
   6.460 -(*functional to print a sequence, up to "count" elements;
   6.461 -  the function prelem should print the element number and also the element*)
   6.462 -fun print prelem count seq =
   6.463 -    let
   6.464 -        fun pr k xq =
   6.465 -            if k > count
   6.466 -            then ()
   6.467 -            else
   6.468 -                case getItem xq of
   6.469 -                    NONE => ()
   6.470 -                  | SOME (x, xq') =>
   6.471 -                    (prelem k x;
   6.472 -                     writeln "";
   6.473 -                     pr (k + 1) xq')
   6.474 -    in
   6.475 -        pr 1 seq
   6.476 -    end
   6.477 -
   6.478 -(*accumulating a function over a sequence; this is lazy*)
   6.479 -fun it_right f (xq, yq) =
   6.480 -    let
   6.481 -        fun its s =
   6.482 -            make (fn () =>
   6.483 -                     case getItem s of
   6.484 -                         NONE => getItem yq
   6.485 -                       | SOME (a, s') => getItem(f (a, its s')))
   6.486 -    in
   6.487 -        its xq
   6.488 -    end
   6.489 -
   6.490 -(*map over a sequence s1, append the sequence s2*)
   6.491 -fun mapp f s1 s2 =
   6.492 -    let
   6.493 -        fun F NONE = getItem s2
   6.494 -          | F (SOME(x,s1')) = SOME(f x,F' s1')
   6.495 -        and F' s = make (fn () => F (getItem s))
   6.496 -    in
   6.497 -        F' s1
   6.498 -    end
   6.499 -
   6.500 -(*turn a list of sequences into a sequence of lists*)
   6.501 -local
   6.502 -    fun F [] = SOME([],Seq (Lazy.value NONE))
   6.503 -      | F (xq :: xqs) =
   6.504 -        case getItem xq of
   6.505 -            NONE => NONE
   6.506 -          | SOME (x, xq') =>
   6.507 -            (case F xqs of
   6.508 -                 NONE => NONE
   6.509 -               | SOME (xs, xsq) =>
   6.510 -                 let
   6.511 -                     fun G s =
   6.512 -                         make (fn () =>
   6.513 -                                  case getItem s of
   6.514 -                                      NONE => F (xq' :: xqs)
   6.515 -                                    | SOME(ys,ysq) => SOME(x::ys,G ysq))
   6.516 -                 in
   6.517 -                     SOME (x :: xs, G xsq)
   6.518 -                 end)
   6.519 -in
   6.520 -fun commute xqs = make (fn () => F xqs)
   6.521 -end
   6.522 -
   6.523 -(*the list of the first n elements, paired with rest of sequence;
   6.524 -  if length of list is less than n, then sequence had less than n elements*)
   6.525 -fun chop (n, xq) =
   6.526 -    if n <= 0
   6.527 -    then ([], xq)
   6.528 -    else
   6.529 -        case getItem xq of
   6.530 -            NONE => ([], xq)
   6.531 -          | SOME (x, xq') => apfst (Basics.cons x) (chop (n - 1, xq'))
   6.532 -
   6.533 -fun foldl f e s =
   6.534 -    let
   6.535 -        fun F k NONE = k e
   6.536 -          | F k (SOME(x,s)) = F (fn y => k (f(x,y))) (getItem s)
   6.537 -    in
   6.538 -        F (fn x => x) (getItem s)
   6.539 -    end
   6.540 -
   6.541 -fun foldr f e s =
   6.542 -    let
   6.543 -        fun F e NONE = e
   6.544 -          | F e (SOME(x,s)) = F (f(x,e)) (getItem s)
   6.545 -    in
   6.546 -        F e (getItem s)
   6.547 -    end
   6.548 -
   6.549 -fun fromString s = of_list (raw_explode s)
   6.550 -
   6.551 -end
   6.552 -
   6.553 -structure LazyScan = Scanner (structure Seq = LazySeq)
   6.554 -
     7.1 --- a/src/HOL/Import/mono_scan.ML	Wed Jul 20 08:46:17 2011 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,237 +0,0 @@
     7.4 -(*  Title:      HOL/Import/mono_scan.ML
     7.5 -    Author:     Steven Obua, TU Muenchen
     7.6 -
     7.7 -Monomorphic scanner combinators for monomorphic sequences.
     7.8 -*)
     7.9 -
    7.10 -signature MONO_SCANNER =
    7.11 -sig
    7.12 -
    7.13 -    include MONO_SCANNER_SEQ
    7.14 -
    7.15 -    exception SyntaxError
    7.16 -
    7.17 -    type 'a scanner = seq -> 'a * seq
    7.18 -
    7.19 -    val :--      : 'a scanner * ('a -> 'b scanner)
    7.20 -                   -> ('a*'b) scanner
    7.21 -    val --       : 'a scanner * 'b scanner -> ('a * 'b) scanner
    7.22 -    val >>       : 'a scanner * ('a -> 'b) -> 'b scanner
    7.23 -    val --|      : 'a scanner * 'b scanner -> 'a scanner
    7.24 -    val |--      : 'a scanner * 'b scanner -> 'b scanner
    7.25 -    val ^^       : string scanner * string scanner
    7.26 -                   -> string scanner 
    7.27 -    val ||       : 'a scanner * 'a scanner -> 'a scanner
    7.28 -    val one      : (item -> bool) -> item scanner
    7.29 -    val anyone   : item scanner
    7.30 -    val succeed  : 'a -> 'a scanner
    7.31 -    val any      : (item -> bool) -> item list scanner
    7.32 -    val any1     : (item -> bool) -> item list scanner
    7.33 -    val optional : 'a scanner -> 'a -> 'a scanner
    7.34 -    val option   : 'a scanner -> 'a option scanner
    7.35 -    val repeat   : 'a scanner -> 'a list scanner
    7.36 -    val repeat1  : 'a scanner -> 'a list scanner
    7.37 -    val repeat_fixed : int -> 'a scanner -> 'a list scanner  
    7.38 -    val ahead    : 'a scanner -> 'a scanner
    7.39 -    val unless   : 'a scanner -> 'b scanner -> 'b scanner
    7.40 -    val !!       : (seq -> string) -> 'a scanner -> 'a scanner
    7.41 -
    7.42 -end
    7.43 -
    7.44 -signature STRING_SCANNER =
    7.45 -sig
    7.46 -
    7.47 -    include MONO_SCANNER  where type item = string
    7.48 -
    7.49 -    val $$       : item -> item scanner
    7.50 -    
    7.51 -    val scan_id : string scanner
    7.52 -    val scan_nat : int scanner
    7.53 -
    7.54 -    val this : item list -> item list scanner
    7.55 -    val this_string : string -> string scanner                                      
    7.56 -
    7.57 -end    
    7.58 -
    7.59 -functor MonoScanner (structure Seq : MONO_SCANNER_SEQ) : MONO_SCANNER =
    7.60 -struct
    7.61 -
    7.62 -infix 7 |-- --|
    7.63 -infix 5 :-- -- ^^
    7.64 -infix 3 >>
    7.65 -infix 0 ||
    7.66 -
    7.67 -exception SyntaxError
    7.68 -exception Fail of string
    7.69 -
    7.70 -type seq = Seq.seq
    7.71 -type item = Seq.item
    7.72 -type 'a scanner = seq -> 'a * seq
    7.73 -
    7.74 -val pull = Seq.pull
    7.75 -
    7.76 -fun (sc1 :-- sc2) toks =
    7.77 -    let
    7.78 -        val (x,toks2) = sc1 toks
    7.79 -        val (y,toks3) = sc2 x toks2
    7.80 -    in
    7.81 -        ((x,y),toks3)
    7.82 -    end
    7.83 -
    7.84 -fun (sc1 -- sc2) toks =
    7.85 -    let
    7.86 -        val (x,toks2) = sc1 toks
    7.87 -        val (y,toks3) = sc2 toks2
    7.88 -    in
    7.89 -        ((x,y),toks3)
    7.90 -    end
    7.91 -
    7.92 -fun (sc >> f) toks =
    7.93 -    let
    7.94 -        val (x,toks2) = sc toks
    7.95 -    in
    7.96 -        (f x,toks2)
    7.97 -    end
    7.98 -
    7.99 -fun (sc1 --| sc2) toks =
   7.100 -    let
   7.101 -        val (x,toks2) = sc1 toks
   7.102 -        val (_,toks3) = sc2 toks2
   7.103 -    in
   7.104 -        (x,toks3)
   7.105 -    end
   7.106 -
   7.107 -fun (sc1 |-- sc2) toks =
   7.108 -    let
   7.109 -        val (_,toks2) = sc1 toks
   7.110 -    in
   7.111 -        sc2 toks2
   7.112 -    end
   7.113 -
   7.114 -fun (sc1 ^^ sc2) toks =
   7.115 -    let
   7.116 -        val (x,toks2) = sc1 toks
   7.117 -        val (y,toks3) = sc2 toks2
   7.118 -    in
   7.119 -        (x^y,toks3)
   7.120 -    end
   7.121 -
   7.122 -fun (sc1 || sc2) toks =
   7.123 -    (sc1 toks)
   7.124 -    handle SyntaxError => sc2 toks
   7.125 -
   7.126 -fun anyone toks = case pull toks of NONE => raise SyntaxError | SOME x => x
   7.127 -
   7.128 -fun one p toks = case anyone toks of x as (t, toks) => if p t then x else raise SyntaxError
   7.129 -
   7.130 -fun succeed e toks = (e,toks)
   7.131 -
   7.132 -fun any p toks =
   7.133 -    case pull toks of
   7.134 -        NONE =>  ([],toks)
   7.135 -      | SOME(x,toks2) => if p x
   7.136 -                         then
   7.137 -                             let
   7.138 -                                 val (xs,toks3) = any p toks2
   7.139 -                             in
   7.140 -                                 (x::xs,toks3)
   7.141 -                             end
   7.142 -                         else ([],toks)
   7.143 -
   7.144 -fun any1 p toks =
   7.145 -    let
   7.146 -        val (x,toks2) = one p toks
   7.147 -        val (xs,toks3) = any p toks2
   7.148 -    in
   7.149 -        (x::xs,toks3)
   7.150 -    end
   7.151 -
   7.152 -fun optional sc def =  sc || succeed def
   7.153 -fun option sc = (sc >> SOME) || succeed NONE
   7.154 -
   7.155 -(*
   7.156 -fun repeat sc =
   7.157 -    let
   7.158 -        fun R toks =
   7.159 -            let
   7.160 -                val (x,toks2) = sc toks
   7.161 -                val (xs,toks3) = R toks2
   7.162 -            in
   7.163 -                (x::xs,toks3)
   7.164 -            end
   7.165 -            handle SyntaxError => ([],toks)
   7.166 -    in
   7.167 -        R
   7.168 -    end
   7.169 -*)
   7.170 -
   7.171 -(* A tail-recursive version of repeat.  It is (ever so) slightly slower
   7.172 - * than the above, non-tail-recursive version (due to the garbage generation
   7.173 - * associated with the reversal of the list).  However,  this version will be
   7.174 - * able to process input where the former version must give up (due to stack
   7.175 - * overflow).  The slowdown seems to be around the one percent mark.
   7.176 - *)
   7.177 -fun repeat sc =
   7.178 -    let
   7.179 -        fun R xs toks =
   7.180 -            case SOME (sc toks) handle SyntaxError => NONE of
   7.181 -                SOME (x,toks2) => R (x::xs) toks2
   7.182 -              | NONE => (List.rev xs,toks)
   7.183 -    in
   7.184 -        R []
   7.185 -    end
   7.186 -
   7.187 -fun repeat1 sc toks =
   7.188 -    let
   7.189 -        val (x,toks2) = sc toks
   7.190 -        val (xs,toks3) = repeat sc toks2
   7.191 -    in
   7.192 -        (x::xs,toks3)
   7.193 -    end
   7.194 -
   7.195 -fun repeat_fixed n sc =
   7.196 -    let
   7.197 -        fun R n xs toks =
   7.198 -            if (n <= 0) then (List.rev xs, toks)
   7.199 -            else case (sc toks) of (x, toks2) => R (n-1) (x::xs) toks2
   7.200 -    in
   7.201 -        R n []
   7.202 -    end
   7.203 -
   7.204 -fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
   7.205 -
   7.206 -fun unless test sc toks =
   7.207 -    let
   7.208 -        val test_failed = (test toks;false) handle SyntaxError => true
   7.209 -    in
   7.210 -        if test_failed
   7.211 -        then sc toks
   7.212 -        else raise SyntaxError
   7.213 -    end
   7.214 -
   7.215 -fun !! f sc toks = (sc toks
   7.216 -                    handle SyntaxError => raise Fail (f toks))
   7.217 -
   7.218 -end
   7.219 -
   7.220 -
   7.221 -structure StringScanner : STRING_SCANNER =
   7.222 -struct
   7.223 -
   7.224 -structure Scan = MonoScanner(structure Seq = StringScannerSeq)
   7.225 -open Scan
   7.226 -
   7.227 -fun $$ arg = one (fn x => x = arg)
   7.228 -
   7.229 -val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode);
   7.230 -
   7.231 -val nat_of_list = the o Int.fromString o implode 
   7.232 -
   7.233 -val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list 
   7.234 -
   7.235 -fun this [] = (fn toks => ([], toks))
   7.236 -  | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
   7.237 -
   7.238 -fun this_string s = this (raw_explode s) >> K s
   7.239 -
   7.240 -end
   7.241 \ No newline at end of file
     8.1 --- a/src/HOL/Import/mono_seq.ML	Wed Jul 20 08:46:17 2011 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,76 +0,0 @@
     8.4 -(*  Title:      HOL/Import/mono_seq.ML
     8.5 -    Author:     Steven Obua, TU Muenchen
     8.6 -
     8.7 -Monomorphic sequences.
     8.8 -*)
     8.9 -
    8.10 -(* The trouble is that signature / structures cannot depend on type variable parameters ... *)
    8.11 -
    8.12 -signature MONO_SCANNER_SEQ =
    8.13 -sig
    8.14 -    type seq
    8.15 -    type item
    8.16 -    
    8.17 -    val pull : seq -> (item * seq) option 
    8.18 -end
    8.19 -
    8.20 -signature MONO_EXTENDED_SCANNER_SEQ =
    8.21 -sig
    8.22 -
    8.23 -  include MONO_SCANNER_SEQ
    8.24 -
    8.25 -  val null : seq -> bool
    8.26 -  val length : seq -> int
    8.27 -  val take_at_most : seq -> int -> item list
    8.28 -
    8.29 -end
    8.30 -
    8.31 -functor MonoExtendScannerSeq (structure Seq : MONO_SCANNER_SEQ) : MONO_EXTENDED_SCANNER_SEQ =
    8.32 -struct
    8.33 -  
    8.34 -type seq = Seq.seq
    8.35 -type item = Seq.item
    8.36 -val pull = Seq.pull
    8.37 -
    8.38 -fun null s = is_none (pull s)
    8.39 -
    8.40 -fun take_at_most s n = 
    8.41 -    if n <= 0 then [] else
    8.42 -    case pull s of 
    8.43 -        NONE => []
    8.44 -      | SOME (x,s') => x::(take_at_most s' (n-1))
    8.45 -
    8.46 -fun length' s n = 
    8.47 -    case pull s of
    8.48 -        NONE => n
    8.49 -      | SOME (_, s') => length' s' (n+1)
    8.50 -
    8.51 -fun length s = length' s 0
    8.52 -                
    8.53 -end  
    8.54 -
    8.55 -
    8.56 -structure StringScannerSeq : 
    8.57 -          sig 
    8.58 -              include MONO_EXTENDED_SCANNER_SEQ 
    8.59 -              val fromString : string -> seq
    8.60 -          end
    8.61 -  =
    8.62 -struct
    8.63 -
    8.64 -structure Incubator : MONO_SCANNER_SEQ =
    8.65 -struct
    8.66 -
    8.67 -type seq = string * int * int
    8.68 -type item = string
    8.69 -
    8.70 -fun pull (s, len, i) = if i >= len then NONE else SOME (String.substring (s, i, 1), (s, len, i+1))
    8.71 -end
    8.72 -
    8.73 -structure Extended = MonoExtendScannerSeq (structure Seq = Incubator)
    8.74 -open Extended
    8.75 -
    8.76 -fun fromString s = (s, String.size s, 0)
    8.77 -
    8.78 -end
    8.79 -
     9.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Jul 20 08:46:17 2011 +0200
     9.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Jul 20 10:11:08 2011 +0200
     9.3 @@ -129,7 +129,7 @@
     9.4  fun to_hol_thm th = HOLThm ([], th)
     9.5  
     9.6  val replay_add_dump = add_dump
     9.7 -fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy)
     9.8 +fun add_dump s thy = replay_add_dump s thy
     9.9  
    9.10  datatype proof_info
    9.11    = Info of {disk_info: (string * string) option Unsynchronized.ref}
    9.12 @@ -303,85 +303,14 @@
    9.13                               handle PK _ => thyname)
    9.14  val get_name : (string * string) list -> string = Lib.assoc "n"
    9.15  
    9.16 -local
    9.17 -    open LazyScan
    9.18 -    infix 7 |-- --|
    9.19 -    infix 5 :-- -- ^^
    9.20 -    infix 3 >>
    9.21 -    infix 0 ||
    9.22 -in
    9.23  exception XML of string
    9.24  
    9.25  datatype xml = Elem of string * (string * string) list * xml list
    9.26  datatype XMLtype = XMLty of xml | FullType of hol_type
    9.27  datatype XMLterm = XMLtm of xml | FullTerm of term
    9.28  
    9.29 -fun pair x y = (x,y)
    9.30 -
    9.31 -fun scan_id toks =
    9.32 -    let
    9.33 -        val (x,toks2) = one Char.isAlpha toks
    9.34 -        val (xs,toks3) = any Char.isAlphaNum toks2
    9.35 -    in
    9.36 -        (String.implode (x::xs),toks3)
    9.37 -    end
    9.38 -
    9.39 -fun scan_string str c =
    9.40 -    let
    9.41 -        fun F [] toks = (c,toks)
    9.42 -          | F (c::cs) toks =
    9.43 -            case LazySeq.getItem toks of
    9.44 -                SOME(c',toks') =>
    9.45 -                if c = c'
    9.46 -                then F cs toks'
    9.47 -                else raise SyntaxError
    9.48 -              | NONE => raise SyntaxError
    9.49 -    in
    9.50 -        F (String.explode str)
    9.51 -    end
    9.52 -
    9.53 -local
    9.54 -    val scan_entity =
    9.55 -        (scan_string "amp;" #"&")
    9.56 -            || scan_string "quot;" #"\""
    9.57 -            || scan_string "gt;" #">"
    9.58 -            || scan_string "lt;" #"<"
    9.59 -            || scan_string "apos;" #"'"
    9.60 -in
    9.61 -fun scan_nonquote toks =
    9.62 -    case LazySeq.getItem toks of
    9.63 -        SOME (c,toks') =>
    9.64 -        (case c of
    9.65 -             #"\"" => raise SyntaxError
    9.66 -           | #"&" => scan_entity toks'
    9.67 -           | c => (c,toks'))
    9.68 -      | NONE => raise SyntaxError
    9.69 -end
    9.70 -
    9.71 -val scan_string = $$ #"\"" |-- repeat scan_nonquote --| $$ #"\"" >>
    9.72 -                     String.implode
    9.73 -
    9.74 -val scan_attribute = scan_id -- $$ #"=" |-- scan_string
    9.75 -
    9.76 -val scan_start_of_tag = $$ #"<" |-- scan_id --
    9.77 -                           repeat ($$ #" " |-- scan_attribute)
    9.78 -
    9.79 -fun scan_end_of_tag toks = ($$ #"/" |-- $$ #">" |-- succeed []) toks
    9.80 -
    9.81 -val scan_end_tag = $$ #"<" |-- $$ #"/" |-- scan_id --| $$ #">"
    9.82 -
    9.83 -fun scan_children id = $$ #">" |-- repeat scan_tag -- scan_end_tag >>
    9.84 -                       (fn (chldr,id') => if id = id'
    9.85 -                                          then chldr
    9.86 -                                          else raise XML "Tag mismatch")
    9.87 -and scan_tag toks =
    9.88 -    let
    9.89 -        val ((id,atts),toks2) = scan_start_of_tag toks
    9.90 -        val (chldr,toks3) = (scan_children id || scan_end_of_tag) toks2
    9.91 -    in
    9.92 -        (Elem (id,atts,chldr),toks3)
    9.93 -    end
    9.94 -end
    9.95 +fun xml_to_import_xml (XML.Elem ((n, l), ts)) = Elem (n, l, map xml_to_import_xml ts)
    9.96 +  | xml_to_import_xml (XML.Text _) = raise XML "Incorrect proof file: text";
    9.97  
    9.98  val type_of = Term.type_of
    9.99  
   9.100 @@ -473,7 +402,6 @@
   9.101        let
   9.102            val _ = Unsynchronized.inc invented_isavar
   9.103            val t = "u_" ^ string_of_int (!invented_isavar)
   9.104 -          val _ = ImportRecorder.protect_varname s t
   9.105            val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames)
   9.106        in
   9.107            t
   9.108 @@ -927,7 +855,7 @@
   9.109  fun import_proof_concl thyname thmname thy =
   9.110      let
   9.111          val is = TextIO.openIn(proof_file_name thyname thmname thy)
   9.112 -        val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
   9.113 +        val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is))
   9.114          val _ = TextIO.closeIn is
   9.115      in
   9.116          case proof_xml of
   9.117 @@ -948,7 +876,7 @@
   9.118  fun import_proof thyname thmname thy =
   9.119      let
   9.120          val is = TextIO.openIn(proof_file_name thyname thmname thy)
   9.121 -        val (proof_xml,_) = scan_tag (LazySeq.of_instream is)
   9.122 +        val proof_xml = xml_to_import_xml (XML.parse (TextIO.inputAll is))
   9.123          val _ = TextIO.closeIn is
   9.124      in
   9.125          case proof_xml of
   9.126 @@ -1292,8 +1220,6 @@
   9.127                          val hth as HOLThm args = mk_res th
   9.128                          val thy' =  thy |> add_hol4_theorem thyname thmname args
   9.129                                          |> add_hol4_mapping thyname thmname isaname
   9.130 -                        val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args)
   9.131 -                        val _ = ImportRecorder.add_hol_mapping thyname thmname isaname
   9.132                      in
   9.133                          (thy',SOME hth)
   9.134                      end
   9.135 @@ -1364,7 +1290,6 @@
   9.136          val rew = rewrite_hol4_term (concl_of th) thy
   9.137          val th  = Thm.equal_elim rew th
   9.138          val thy' = add_hol4_pending thyname thmname args thy
   9.139 -        val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
   9.140          val th = disambiguate_frees th
   9.141          val th = Object_Logic.rulify th
   9.142          val thy2 =
   9.143 @@ -1920,17 +1845,14 @@
   9.144          val csyn = mk_syn thy constname
   9.145          val thy1 = case HOL4DefThy.get thy of
   9.146                         Replaying _ => thy
   9.147 -                     | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)];
   9.148 -                              Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy)
   9.149 +                     | _ => Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy
   9.150          val eq = mk_defeq constname rhs' thy1
   9.151          val (thms, thy2) = Global_Theory.add_defs false [((Binding.name thmname,eq),[])] thy1
   9.152 -        val _ = ImportRecorder.add_defs thmname eq
   9.153          val def_thm = hd thms
   9.154          val thm' = def_thm RS meta_eq_to_obj_eq_thm
   9.155          val (thy',th) = (thy2, thm')
   9.156          val fullcname = Sign.intern_const thy' constname
   9.157          val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
   9.158 -        val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname
   9.159          val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
   9.160          val rew = rewrite_hol4_term eq thy''
   9.161          val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
   9.162 @@ -1958,13 +1880,10 @@
   9.163                      | NONE => raise ERR "new_definition" "Bad conclusion"
   9.164          val fullname = Sign.full_bname thy22 thmname
   9.165          val thy22' = case opt_get_output_thy thy22 of
   9.166 -                         "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
   9.167 -                                add_hol4_mapping thyname thmname fullname thy22)
   9.168 +                         "" => add_hol4_mapping thyname thmname fullname thy22
   9.169                         | output_thy =>
   9.170                           let
   9.171                               val moved_thmname = output_thy ^ "." ^ thyname ^ "." ^ thmname
   9.172 -                             val _ = ImportRecorder.add_hol_move fullname moved_thmname
   9.173 -                             val _ = ImportRecorder.add_hol_mapping thyname thmname moved_thmname
   9.174                           in
   9.175                               thy22 |> add_hol4_move fullname moved_thmname
   9.176                                     |> add_hol4_mapping thyname thmname moved_thmname
   9.177 @@ -2012,7 +1931,6 @@
   9.178                                     acc ^ "\n  " ^ quotename c ^ " :: \"" ^
   9.179                                     Syntax.string_of_typ_global thy T ^ "\" " ^ string_of_mixfix csyn) ("consts", consts)
   9.180                                 val thy' = add_dump str thy
   9.181 -                               val _ = ImportRecorder.add_consts consts
   9.182                             in
   9.183                                 Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy'
   9.184                             end
   9.185 @@ -2024,7 +1942,6 @@
   9.186              val (thy',res) = Choice_Specification.add_specification NONE
   9.187                                   names'
   9.188                                   (thy1,th)
   9.189 -            val _ = ImportRecorder.add_specification names' th
   9.190              val res' = Thm.unvarify_global res
   9.191              val hth = HOLThm(rens,res')
   9.192              val rew = rewrite_hol4_term (concl_of res') thy'
   9.193 @@ -2092,19 +2009,16 @@
   9.194              val ((_, typedef_info), thy') =
   9.195                Typedef.add_typedef_global false (SOME (Binding.name thmname))
   9.196                  (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c NONE (rtac th2 1) thy
   9.197 -            val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2
   9.198  
   9.199              val th3 = (#type_definition (#2 typedef_info)) RS typedef_hol2hol4
   9.200  
   9.201              val fulltyname = Sign.intern_type thy' tycname
   9.202              val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
   9.203 -            val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
   9.204  
   9.205              val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th3))
   9.206              val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variable-disambiguating")
   9.207                      else ()
   9.208              val thy4 = add_hol4_pending thyname thmname args thy''
   9.209 -            val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
   9.210  
   9.211              val rew = rewrite_hol4_term (concl_of td_th) thy4
   9.212              val th  = Thm.equal_elim rew (Thm.transfer thy4 td_th)
   9.213 @@ -2169,7 +2083,6 @@
   9.214                Typedef.add_typedef_global false NONE
   9.215                  (Binding.name tycname, map (rpair dummyS) tnames, tsyn) c
   9.216                  (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy
   9.217 -            val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2
   9.218              val fulltyname = Sign.intern_type thy' tycname
   9.219              val aty = Type (fulltyname, map mk_vartype tnames)
   9.220              val abs_ty = tT --> aty
   9.221 @@ -2186,11 +2099,9 @@
   9.222                raise ERR "type_introduction" "no term variables expected any more"
   9.223              val _ = message ("step 3: thyname="^thyname^", tycname="^tycname^", fulltyname="^fulltyname)
   9.224              val thy'' = add_hol4_type_mapping thyname tycname true fulltyname thy'
   9.225 -            val _ = ImportRecorder.add_hol_type_mapping thyname tycname fulltyname
   9.226              val _ = message "step 4"
   9.227              val (hth' as HOLThm args) = norm_hthm thy'' (HOLThm(rens,th4))
   9.228              val thy4 = add_hol4_pending thyname thmname args thy''
   9.229 -            val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth')
   9.230  
   9.231              val P' = P (* why !? #2 (Logic.dest_equals (concl_of (rewrite_hol4_term P thy4))) *)
   9.232              val c   =
    10.1 --- a/src/HOL/Import/replay.ML	Wed Jul 20 08:46:17 2011 +0200
    10.2 +++ b/src/HOL/Import/replay.ML	Wed Jul 20 10:11:08 2011 +0200
    10.3 @@ -6,7 +6,6 @@
    10.4  struct
    10.5  
    10.6  open ProofKernel
    10.7 -open ImportRecorder
    10.8  
    10.9  exception REPLAY of string * string
   10.10  fun ERR f mesg = REPLAY (f,mesg)
   10.11 @@ -14,7 +13,6 @@
   10.12  
   10.13  fun replay_proof int_thms thyname thmname prf thy =
   10.14      let
   10.15 -        val _ = ImportRecorder.start_replay_proof thyname thmname 
   10.16          fun rp (PRefl tm) thy = ProofKernel.REFL tm thy
   10.17            | rp (PInstT(p,lambda)) thy =
   10.18              let
   10.19 @@ -269,13 +267,8 @@
   10.20                    | _ => rp pc thy
   10.21              end
   10.22      in
   10.23 -        let
   10.24 -            val x = rp' prf thy
   10.25 -            val _ = ImportRecorder.stop_replay_proof thyname thmname
   10.26 -        in
   10.27 -            x
   10.28 -        end
   10.29 -    end handle x => (ImportRecorder.abort_replay_proof thyname thmname; reraise x)  (* FIXME avoid handle x ?? *)
   10.30 +        rp' prf thy
   10.31 +    end
   10.32  
   10.33  fun setup_int_thms thyname thy =
   10.34      let
   10.35 @@ -316,74 +309,8 @@
   10.36          replay_fact (thmname,thy)
   10.37      end
   10.38  
   10.39 -fun replay_chached_thm int_thms thyname thmname =
   10.40 -    let
   10.41 -        fun th_of thy = Skip_Proof.make_thm thy
   10.42 -        fun err msg = raise ERR "replay_cached_thm" msg
   10.43 -        val _ = writeln ("Replaying (from cache) "^thmname^" ...")
   10.44 -        fun rps [] thy = thy
   10.45 -          | rps (t::ts) thy = rps ts (rp t thy)
   10.46 -        and rp (ThmEntry (thyname', thmname', aborted, History history)) thy = rps history thy      
   10.47 -          | rp (DeltaEntry ds) thy = fold delta ds thy
   10.48 -        and delta (Specification (names, th)) thy = 
   10.49 -            fst (Choice_Specification.add_specification NONE names (thy,th_of thy th))
   10.50 -          | delta (Hol_mapping (thyname, thmname, isaname)) thy = 
   10.51 -            add_hol4_mapping thyname thmname isaname thy
   10.52 -          | delta (Hol_pending (thyname, thmname, th)) thy = 
   10.53 -            add_hol4_pending thyname thmname ([], th_of thy th) thy
   10.54 -          | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy
   10.55 -          | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = 
   10.56 -            add_hol4_const_mapping thyname constname true fullcname thy
   10.57 -          | delta (Hol_move (fullname, moved_thmname)) thy = 
   10.58 -            add_hol4_move fullname moved_thmname thy
   10.59 -          | delta (Defs (thmname, eq)) thy =
   10.60 -            snd (Global_Theory.add_defs false [((Binding.name thmname, eq), [])] thy)
   10.61 -          | delta (Hol_theorem (thyname, thmname, th)) thy =
   10.62 -            add_hol4_theorem thyname thmname ([], th_of thy th) thy
   10.63 -          | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = 
   10.64 -            snd (Typedef.add_typedef_global false (Option.map Binding.name thmname)
   10.65 -              (Binding.name t, map (rpair dummyS) vs, mx) c
   10.66 -        (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy)
   10.67 -          | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy =  
   10.68 -            add_hol4_type_mapping thyname tycname true fulltyname thy
   10.69 -          | delta (Indexed_theorem (i, th)) thy = 
   10.70 -            (Array.update (int_thms,i-1,SOME (ProofKernel.to_hol_thm (th_of thy th))); thy)                   
   10.71 -          | delta (Protect_varname (s,t)) thy = (ProofKernel.replay_protect_varname s t; thy)
   10.72 -          | delta (Dump s) thy = ProofKernel.replay_add_dump s thy
   10.73 -    in
   10.74 -        rps
   10.75 -    end
   10.76 -
   10.77  fun import_thms thyname int_thms thmnames thy =
   10.78      let
   10.79 -        fun zip names [] = ([], names)
   10.80 -          | zip [] _ = ([], [])
   10.81 -          | zip (thmname::names) ((ThmEntry (entry as (thyname',thmname',aborted,History history)))::ys) = 
   10.82 -            if thyname = thyname' andalso thmname = thmname' then
   10.83 -                (if aborted then ([], thmname::names) else 
   10.84 -                 let
   10.85 -                     val _ = writeln ("theorem is in-sync: "^thmname)
   10.86 -                     val (cached,normal) = zip names ys
   10.87 -                 in
   10.88 -                     (entry::cached, normal)
   10.89 -                 end)
   10.90 -            else
   10.91 -                let
   10.92 -                    val _ = writeln ("cached theorems are not in-sync,  expected: "^thmname^", found: "^thmname')
   10.93 -                    val _ = writeln ("proceeding with next uncached theorem...")
   10.94 -                in
   10.95 -                    ([], thmname::names)
   10.96 -                end
   10.97 -        (*      raise ERR "import_thms" ("cached theorems are not in-sync, expected: "^thmname^", found: "^thmname')*)
   10.98 -          | zip (thmname::_) (DeltaEntry _ :: _) = 
   10.99 -            raise ERR "import_thms" ("expected theorem '"^thmname^"', but found a delta")
  10.100 -        fun zip' xs (History ys) = 
  10.101 -            let
  10.102 -                val _ = writeln ("length of xs: "^(string_of_int (length xs)))
  10.103 -                val _ = writeln ("length of history: "^(string_of_int (length ys)))
  10.104 -            in
  10.105 -                zip xs ys
  10.106 -            end
  10.107          fun replay_fact thmname thy = 
  10.108              let
  10.109                  val prf = mk_proof PDisk        
  10.110 @@ -393,10 +320,7 @@
  10.111              in
  10.112                  p
  10.113              end
  10.114 -        fun replay_cache (_,thmname, _, History history) thy = replay_chached_thm int_thms thyname thmname history thy
  10.115 -        val (cached, normal) = zip' thmnames (ImportRecorder.get_history ())
  10.116 -        val _ = ImportRecorder.set_history (History (map ThmEntry cached))
  10.117 -        val res_thy = fold replay_fact normal (fold replay_cache cached thy)
  10.118 +        val res_thy = fold replay_fact thmnames thy
  10.119      in
  10.120          res_thy
  10.121      end
    11.1 --- a/src/HOL/Import/scan.ML	Wed Jul 20 08:46:17 2011 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,219 +0,0 @@
    11.4 -(*  Title:      HOL/Import/scan.ML
    11.5 -    Author:     Sebastian Skalberg, TU Muenchen / Steven Obua, TU Muenchen
    11.6 -
    11.7 -Scanner combinators for sequences.
    11.8 -*)
    11.9 -
   11.10 -signature SCANNER =
   11.11 -sig
   11.12 -
   11.13 -    include SCANNER_SEQ
   11.14 -
   11.15 -    exception SyntaxError
   11.16 -
   11.17 -    type ('a,'b) scanner = 'a seq -> 'b * 'a seq
   11.18 -
   11.19 -    val :--      : ('a,'b) scanner * ('b -> ('a,'c) scanner)
   11.20 -                   -> ('a,'b*'c) scanner
   11.21 -    val --       : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner
   11.22 -    val >>       : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner
   11.23 -    val --|      : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner
   11.24 -    val |--      : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner
   11.25 -    val ^^       : ('a,string) scanner * ('a,string) scanner
   11.26 -                   -> ('a,string) scanner 
   11.27 -    val ||       : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner
   11.28 -    val one      : ('a -> bool) -> ('a,'a) scanner
   11.29 -    val anyone   : ('a,'a) scanner
   11.30 -    val succeed  : 'b -> ('a,'b) scanner
   11.31 -    val any      : ('a -> bool) -> ('a,'a list) scanner
   11.32 -    val any1     : ('a -> bool) -> ('a,'a list) scanner
   11.33 -    val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner
   11.34 -    val option   : ('a,'b) scanner -> ('a,'b option) scanner
   11.35 -    val repeat   : ('a,'b) scanner -> ('a,'b list) scanner
   11.36 -    val repeat1  : ('a,'b) scanner -> ('a,'b list) scanner
   11.37 -    val repeat_fixed : int -> ('a, 'b) scanner -> ('a, 'b list) scanner  
   11.38 -    val ahead    : ('a,'b) scanner -> ('a,'b) scanner
   11.39 -    val unless   : ('a, 'b) scanner -> ('a,'c) scanner -> ('a,'c) scanner
   11.40 -    val $$       : ''a -> (''a,''a) scanner
   11.41 -    val !!       : ('a seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner
   11.42 -    
   11.43 -    val scan_id : (string, string) scanner
   11.44 -    val scan_nat : (string, int) scanner
   11.45 -
   11.46 -    val this : ''a list -> (''a, ''a list) scanner
   11.47 -    val this_string : string -> (string, string) scanner
   11.48 -end
   11.49 -
   11.50 -functor Scanner (structure Seq : SCANNER_SEQ) : SCANNER =
   11.51 -struct
   11.52 -
   11.53 -infix 7 |-- --|
   11.54 -infix 5 :-- -- ^^
   11.55 -infix 3 >>
   11.56 -infix 0 ||
   11.57 -
   11.58 -exception SyntaxError
   11.59 -exception Fail of string
   11.60 -
   11.61 -type 'a seq = 'a Seq.seq
   11.62 -type ('a,'b) scanner = 'a seq -> 'b * 'a seq
   11.63 -
   11.64 -val pull = Seq.pull
   11.65 -
   11.66 -fun (sc1 :-- sc2) toks =
   11.67 -    let
   11.68 -        val (x,toks2) = sc1 toks
   11.69 -        val (y,toks3) = sc2 x toks2
   11.70 -    in
   11.71 -        ((x,y),toks3)
   11.72 -    end
   11.73 -
   11.74 -fun (sc1 -- sc2) toks =
   11.75 -    let
   11.76 -        val (x,toks2) = sc1 toks
   11.77 -        val (y,toks3) = sc2 toks2
   11.78 -    in
   11.79 -        ((x,y),toks3)
   11.80 -    end
   11.81 -
   11.82 -fun (sc >> f) toks =
   11.83 -    let
   11.84 -        val (x,toks2) = sc toks
   11.85 -    in
   11.86 -        (f x,toks2)
   11.87 -    end
   11.88 -
   11.89 -fun (sc1 --| sc2) toks =
   11.90 -    let
   11.91 -        val (x,toks2) = sc1 toks
   11.92 -        val (_,toks3) = sc2 toks2
   11.93 -    in
   11.94 -        (x,toks3)
   11.95 -    end
   11.96 -
   11.97 -fun (sc1 |-- sc2) toks =
   11.98 -    let
   11.99 -        val (_,toks2) = sc1 toks
  11.100 -    in
  11.101 -        sc2 toks2
  11.102 -    end
  11.103 -
  11.104 -fun (sc1 ^^ sc2) toks =
  11.105 -    let
  11.106 -        val (x,toks2) = sc1 toks
  11.107 -        val (y,toks3) = sc2 toks2
  11.108 -    in
  11.109 -        (x^y,toks3)
  11.110 -    end
  11.111 -
  11.112 -fun (sc1 || sc2) toks =
  11.113 -    (sc1 toks)
  11.114 -    handle SyntaxError => sc2 toks
  11.115 -
  11.116 -fun anyone toks = case pull toks of NONE => raise SyntaxError | SOME x => x
  11.117 -
  11.118 -fun one p toks = case anyone toks of x as (t, toks) => if p t then x else raise SyntaxError
  11.119 -
  11.120 -fun succeed e toks = (e,toks)
  11.121 -
  11.122 -fun any p toks =
  11.123 -    case pull toks of
  11.124 -        NONE =>  ([],toks)
  11.125 -      | SOME(x,toks2) => if p x
  11.126 -                         then
  11.127 -                             let
  11.128 -                                 val (xs,toks3) = any p toks2
  11.129 -                             in
  11.130 -                                 (x::xs,toks3)
  11.131 -                             end
  11.132 -                         else ([],toks)
  11.133 -
  11.134 -fun any1 p toks =
  11.135 -    let
  11.136 -        val (x,toks2) = one p toks
  11.137 -        val (xs,toks3) = any p toks2
  11.138 -    in
  11.139 -        (x::xs,toks3)
  11.140 -    end
  11.141 -
  11.142 -fun optional sc def =  sc || succeed def
  11.143 -fun option sc = (sc >> SOME) || succeed NONE
  11.144 -
  11.145 -(*
  11.146 -fun repeat sc =
  11.147 -    let
  11.148 -        fun R toks =
  11.149 -            let
  11.150 -                val (x,toks2) = sc toks
  11.151 -                val (xs,toks3) = R toks2
  11.152 -            in
  11.153 -                (x::xs,toks3)
  11.154 -            end
  11.155 -            handle SyntaxError => ([],toks)
  11.156 -    in
  11.157 -        R
  11.158 -    end
  11.159 -*)
  11.160 -
  11.161 -(* A tail-recursive version of repeat.  It is (ever so) slightly slower
  11.162 - * than the above, non-tail-recursive version (due to the garbage generation
  11.163 - * associated with the reversal of the list).  However,  this version will be
  11.164 - * able to process input where the former version must give up (due to stack
  11.165 - * overflow).  The slowdown seems to be around the one percent mark.
  11.166 - *)
  11.167 -fun repeat sc =
  11.168 -    let
  11.169 -        fun R xs toks =
  11.170 -            case SOME (sc toks) handle SyntaxError => NONE of
  11.171 -                SOME (x,toks2) => R (x::xs) toks2
  11.172 -              | NONE => (List.rev xs,toks)
  11.173 -    in
  11.174 -        R []
  11.175 -    end
  11.176 -
  11.177 -fun repeat1 sc toks =
  11.178 -    let
  11.179 -        val (x,toks2) = sc toks
  11.180 -        val (xs,toks3) = repeat sc toks2
  11.181 -    in
  11.182 -        (x::xs,toks3)
  11.183 -    end
  11.184 -
  11.185 -fun repeat_fixed n sc =
  11.186 -    let
  11.187 -        fun R n xs toks =
  11.188 -            if (n <= 0) then (List.rev xs, toks)
  11.189 -            else case (sc toks) of (x, toks2) => R (n-1) (x::xs) toks2
  11.190 -    in
  11.191 -        R n []
  11.192 -    end
  11.193 -
  11.194 -fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks)
  11.195 -
  11.196 -fun unless test sc toks =
  11.197 -    let
  11.198 -        val test_failed = (test toks;false) handle SyntaxError => true
  11.199 -    in
  11.200 -        if test_failed
  11.201 -        then sc toks
  11.202 -        else raise SyntaxError
  11.203 -    end
  11.204 -
  11.205 -fun $$ arg = one (fn x => x = arg)
  11.206 -
  11.207 -fun !! f sc toks = (sc toks
  11.208 -                    handle SyntaxError => raise Fail (f toks))
  11.209 -
  11.210 -val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode);
  11.211 -
  11.212 -val nat_of_list = the o Int.fromString o implode 
  11.213 -
  11.214 -val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list 
  11.215 -
  11.216 -fun this [] = (fn toks => ([], toks))
  11.217 -  | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
  11.218 -
  11.219 -fun this_string s = this (raw_explode s) >> K s
  11.220 -
  11.221 -end
  11.222 -
    12.1 --- a/src/HOL/Import/seq.ML	Wed Jul 20 08:46:17 2011 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,99 +0,0 @@
    12.4 -signature SCANNER_SEQ =
    12.5 -sig
    12.6 -    type 'a seq
    12.7 -    
    12.8 -    val pull : 'a seq -> ('a * 'a seq) option 
    12.9 -end
   12.10 -
   12.11 -signature EXTENDED_SCANNER_SEQ =
   12.12 -sig
   12.13 -
   12.14 -  include SCANNER_SEQ
   12.15 -
   12.16 -  val null : 'a seq -> bool
   12.17 -  val length : 'a seq -> int
   12.18 -  val take_at_most : 'a seq -> int -> 'a list
   12.19 -
   12.20 -end
   12.21 -
   12.22 -functor ExtendScannerSeq (structure Seq : SCANNER_SEQ) : EXTENDED_SCANNER_SEQ =
   12.23 -struct
   12.24 -  
   12.25 -type 'a seq = 'a Seq.seq
   12.26 -
   12.27 -val pull = Seq.pull
   12.28 -
   12.29 -fun null s = is_none (pull s)
   12.30 -
   12.31 -fun take_at_most s n = 
   12.32 -    if n <= 0 then [] else
   12.33 -    case pull s of 
   12.34 -        NONE => []
   12.35 -      | SOME (x,s') => x::(take_at_most s' (n-1))
   12.36 -
   12.37 -fun length' s n = 
   12.38 -    case pull s of
   12.39 -        NONE => n
   12.40 -      | SOME (_, s') => length' s' (n+1)
   12.41 -
   12.42 -fun length s = length' s 0
   12.43 -                
   12.44 -end  
   12.45 -
   12.46 -signature VECTOR_SCANNER_SEQ = 
   12.47 -sig
   12.48 -    include EXTENDED_SCANNER_SEQ
   12.49 -
   12.50 -    val fromString : string -> string seq
   12.51 -    val fromVector : 'a Vector.vector -> 'a seq
   12.52 -end
   12.53 -
   12.54 -structure VectorScannerSeq :> VECTOR_SCANNER_SEQ =
   12.55 -struct
   12.56 -  
   12.57 -structure Incubator : SCANNER_SEQ =
   12.58 -struct
   12.59 -
   12.60 -type 'a seq = 'a Vector.vector * int * int
   12.61 -fun pull (v, len, i) = if i >= len then NONE else SOME (Vector.sub (v, i), (v, len, i+1))
   12.62 -
   12.63 -end
   12.64 -
   12.65 -structure Extended = ExtendScannerSeq (structure Seq = Incubator)
   12.66 -
   12.67 -open Extended
   12.68 -
   12.69 -fun fromVector v = (v, Vector.length v, 0)
   12.70 -fun vector_from_string s = Vector.tabulate (String.size s, fn i => String.str (String.sub (s, i)))
   12.71 -fun fromString s = fromVector (vector_from_string s)
   12.72 -
   12.73 -end
   12.74 -
   12.75 -signature LIST_SCANNER_SEQ =
   12.76 -sig
   12.77 -    include EXTENDED_SCANNER_SEQ
   12.78 -    
   12.79 -    val fromString : string -> string seq
   12.80 -    val fromList : 'a list -> 'a seq
   12.81 -end
   12.82 -
   12.83 -structure ListScannerSeq :> LIST_SCANNER_SEQ =
   12.84 -struct
   12.85 -     
   12.86 -structure Incubator : SCANNER_SEQ =
   12.87 -struct
   12.88 -
   12.89 -type 'a seq = 'a list
   12.90 -fun pull [] = NONE
   12.91 -  | pull (x::xs) = SOME (x, xs)
   12.92 -
   12.93 -end
   12.94 -
   12.95 -structure Extended = ExtendScannerSeq (structure Seq = Incubator)
   12.96 -
   12.97 -open Extended
   12.98 -
   12.99 -val fromList = I
  12.100 -val fromString = raw_explode
  12.101 -
  12.102 -end
    13.1 --- a/src/HOL/Import/xml.ML	Wed Jul 20 08:46:17 2011 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,199 +0,0 @@
    13.4 -(*  Title:      HOL/Import/xml.ML
    13.5 -
    13.6 -Yet another version of XML support.
    13.7 -*)
    13.8 -
    13.9 -signature XML =
   13.10 -sig
   13.11 -  val header: string
   13.12 -  val text: string -> string
   13.13 -  val text_charref: string -> string
   13.14 -  val cdata: string -> string
   13.15 -  val element: string -> (string * string) list -> string list -> string
   13.16 -  
   13.17 -  datatype tree =
   13.18 -      Elem of string * (string * string) list * tree list
   13.19 -    | Text of string
   13.20 -  
   13.21 -  val string_of_tree: tree -> string
   13.22 -  val tree_of_string: string -> tree
   13.23 -
   13.24 -  val encoded_string_of_tree : tree -> string
   13.25 -  val tree_of_encoded_string : string -> tree
   13.26 -end;
   13.27 -
   13.28 -structure XML :> XML =
   13.29 -struct
   13.30 -
   13.31 -(*structure Seq = VectorScannerSeq
   13.32 -structure Scan = Scanner (structure Seq = Seq)*)
   13.33 -structure Seq = StringScannerSeq
   13.34 -structure Scan = StringScanner
   13.35 -
   13.36 -
   13.37 -open Scan
   13.38 -
   13.39 -(** string based representation (small scale) **)
   13.40 -
   13.41 -val header = "<?xml version=\"1.0\"?>\n";
   13.42 -
   13.43 -(* text and character data *)
   13.44 -
   13.45 -fun decode "&lt;" = "<"
   13.46 -  | decode "&gt;" = ">"
   13.47 -  | decode "&amp;" = "&"
   13.48 -  | decode "&apos;" = "'"
   13.49 -  | decode "&quot;" = "\""
   13.50 -  | decode c = c;
   13.51 -
   13.52 -fun encode "<" = "&lt;"
   13.53 -  | encode ">" = "&gt;"
   13.54 -  | encode "&" = "&amp;"
   13.55 -  | encode "'" = "&apos;"
   13.56 -  | encode "\"" = "&quot;"
   13.57 -  | encode c = c;
   13.58 -
   13.59 -fun encode_charref c = "&#" ^ string_of_int (ord c) ^ ";"
   13.60 -
   13.61 -val text = Library.translate_string encode
   13.62 -
   13.63 -val text_charref = translate_string encode_charref;
   13.64 -
   13.65 -val cdata = enclose "<![CDATA[" "]]>\n"
   13.66 -
   13.67 -(* elements *)
   13.68 -
   13.69 -fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
   13.70 -
   13.71 -fun element name atts cs =
   13.72 -  let val elem = space_implode " " (name :: map attribute atts) in
   13.73 -    if null cs then enclose "<" "/>" elem
   13.74 -    else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
   13.75 -  end;
   13.76 -
   13.77 -(** explicit XML trees **)
   13.78 -
   13.79 -datatype tree =
   13.80 -    Elem of string * (string * string) list * tree list
   13.81 -  | Text of string;
   13.82 -
   13.83 -fun string_of_tree tree =
   13.84 -  let
   13.85 -    fun string_of (Elem (name, atts, ts)) buf =
   13.86 -        let val buf' =
   13.87 -          buf |> Buffer.add "<"
   13.88 -          |> fold Buffer.add (separate " " (name :: map attribute atts))
   13.89 -        in
   13.90 -          if null ts then
   13.91 -            buf' |> Buffer.add "/>"
   13.92 -          else
   13.93 -            buf' |> Buffer.add ">"
   13.94 -            |> fold string_of ts
   13.95 -            |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
   13.96 -        end
   13.97 -      | string_of (Text s) buf = Buffer.add (text s) buf;
   13.98 -  in Buffer.content (string_of tree Buffer.empty) end;
   13.99 -
  13.100 -(** XML parsing **)
  13.101 -
  13.102 -fun beginning n xs = Symbol.beginning n (Seq.take_at_most xs n)
  13.103 -
  13.104 -fun err s xs =
  13.105 -  "XML parsing error: " ^ s ^ "\nfound: " ^ quote (beginning 100 xs) ;
  13.106 -
  13.107 -val scan_whspc = Scan.any Symbol.is_blank;
  13.108 -
  13.109 -val scan_special = $$ "&" ^^ scan_id ^^ $$ ";" >> decode;
  13.110 -
  13.111 -val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
  13.112 -  (scan_special || Scan.one Symbol.is_regular)) >> implode;
  13.113 -
  13.114 -val parse_cdata = Scan.this_string "<![CDATA[" |--
  13.115 -  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
  13.116 -    implode) --| Scan.this_string "]]>";
  13.117 -
  13.118 -val parse_att =
  13.119 -    scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
  13.120 -    (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
  13.121 -    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
  13.122 -
  13.123 -val parse_comment = Scan.this_string "<!--" --
  13.124 -  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
  13.125 -  Scan.this_string "-->";
  13.126 -
  13.127 -val scan_comment_whspc = 
  13.128 -    (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
  13.129 -
  13.130 -val parse_pi = Scan.this_string "<?" |--
  13.131 -  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
  13.132 -  Scan.this_string "?>";
  13.133 -
  13.134 -fun parse_content xs =
  13.135 -  ((Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) [] --
  13.136 -    (Scan.repeat ((* scan_whspc |-- *)
  13.137 -       (   parse_elem >> single
  13.138 -        || parse_cdata >> (single o Text)
  13.139 -        || parse_pi >> K []
  13.140 -        || parse_comment >> K []) --
  13.141 -       Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
  13.142 -         >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
  13.143 -
  13.144 -and parse_elem xs =
  13.145 -  ($$ "<" |-- scan_id --
  13.146 -    Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
  13.147 -      !! (err "Expected > or />")
  13.148 -        (Scan.this_string "/>" >> K []
  13.149 -         || $$ ">" |-- parse_content --|
  13.150 -            !! (err ("Expected </" ^ s ^ ">"))
  13.151 -              (Scan.this_string ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
  13.152 -    (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
  13.153 -
  13.154 -val parse_document =
  13.155 -  Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
  13.156 -    (Scan.repeat (Scan.unless ($$ ">")
  13.157 -      (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
  13.158 -  parse_elem;
  13.159 -
  13.160 -fun tree_of_string s =
  13.161 -    let
  13.162 -        val seq = Seq.fromString s
  13.163 -        val scanner = !! (err "Malformed element") (scan_whspc |-- parse_elem --| scan_whspc)
  13.164 -        val (x, toks) = scanner seq
  13.165 -    in
  13.166 -        if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
  13.167 -    end
  13.168 -
  13.169 -(* More efficient saving and loading of xml trees employing a proprietary external format *)
  13.170 -
  13.171 -fun write_lstring s buf = buf |> Buffer.add (string_of_int (size s)) |> Buffer.add " " |> Buffer.add s
  13.172 -fun parse_lstring toks = (scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i (one (K true))) >> snd >> implode) toks
  13.173 -
  13.174 -fun write_list w l buf = buf |> Buffer.add (string_of_int (length l)) |> Buffer.add " " |> fold w l     
  13.175 -fun parse_list sc = scan_nat --| one Symbol.is_blank :-- (fn i => repeat_fixed i sc) >> snd
  13.176 -
  13.177 -fun write_tree (Text s) buf = buf |> Buffer.add "T" |> write_lstring s
  13.178 -  | write_tree (Elem (name, attrs, children)) buf = 
  13.179 -    buf |> Buffer.add "E" 
  13.180 -        |> write_lstring name 
  13.181 -        |> write_list (fn (a,b) => fn buf => buf |> write_lstring a |> write_lstring b) attrs 
  13.182 -        |> write_list write_tree children
  13.183 -
  13.184 -fun parse_tree toks = (one (K true) :-- (fn "T" => parse_lstring >> Text | "E" => parse_elem | _ => raise SyntaxError) >> snd) toks
  13.185 -and parse_elem toks = (parse_lstring -- parse_list (parse_lstring -- parse_lstring) -- parse_list parse_tree >> (fn ((n, a), c) => Elem (n,a,c))) toks
  13.186 -
  13.187 -fun encoded_string_of_tree tree = Buffer.content (write_tree tree Buffer.empty)
  13.188 -
  13.189 -fun tree_of_encoded_string s = 
  13.190 -    let
  13.191 -        fun print (a,b) = writeln (a^" "^(string_of_int b))
  13.192 -        val _ = print ("length of encoded string: ", size s)
  13.193 -        val _ = writeln "Seq.fromString..."
  13.194 -        val seq = timeit (fn () => Seq.fromString s)
  13.195 -        val  _ = print ("length of sequence", timeit (fn () => Seq.length seq))
  13.196 -        val scanner = !! (err "Malformed encoded xml") parse_tree
  13.197 -        val (x, toks) = scanner seq
  13.198 -    in
  13.199 -        if Seq.null toks then x else error ("Unprocessed input: '"^(beginning 100 toks)^"'")
  13.200 -    end        
  13.201 -
  13.202 -end;
    14.1 --- a/src/HOL/Import/xmlconv.ML	Wed Jul 20 08:46:17 2011 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,303 +0,0 @@
    14.4 -signature XML_CONV =
    14.5 -sig
    14.6 -  type 'a input = XML.tree -> 'a
    14.7 -  type 'a output = 'a -> XML.tree
    14.8 -
    14.9 -  exception ParseException of string
   14.10 -
   14.11 -  val xml_of_typ: typ output
   14.12 -  val typ_of_xml: typ input
   14.13 -
   14.14 -  val xml_of_term: term output
   14.15 -  val term_of_xml : term input
   14.16 -
   14.17 -  val xml_of_mixfix: mixfix output
   14.18 -  val mixfix_of_xml: mixfix input
   14.19 -  
   14.20 -  val xml_of_proof: Proofterm.proof output
   14.21 -
   14.22 -  val xml_of_bool: bool output
   14.23 -  val bool_of_xml: bool input
   14.24 -                  
   14.25 -  val xml_of_int: int output
   14.26 -  val int_of_xml: int input
   14.27 -
   14.28 -  val xml_of_string: string output
   14.29 -  val string_of_xml: string input
   14.30 -
   14.31 -  val xml_of_list: 'a output -> 'a list output
   14.32 -  val list_of_xml: 'a input -> 'a list input
   14.33 -  
   14.34 -  val xml_of_tuple : 'a output -> 'a list output
   14.35 -  val tuple_of_xml: 'a input -> int -> 'a list input
   14.36 -
   14.37 -  val xml_of_option: 'a output -> 'a option output
   14.38 -  val option_of_xml: 'a input -> 'a option input
   14.39 -
   14.40 -  val xml_of_pair: 'a output -> 'b output -> ('a * 'b) output
   14.41 -  val pair_of_xml: 'a input -> 'b input -> ('a * 'b) input
   14.42 -
   14.43 -  val xml_of_triple: 'a output -> 'b output -> 'c output -> ('a * 'b * 'c) output
   14.44 -  val triple_of_xml: 'a input -> 'b input -> 'c input -> ('a * 'b * 'c) input
   14.45 -  
   14.46 -  val xml_of_unit: unit output
   14.47 -  val unit_of_xml: unit input
   14.48 -
   14.49 -  val xml_of_quadruple: 'a output -> 'b output -> 'c output -> 'd output -> ('a * 'b * 'c * 'd) output
   14.50 -  val quadruple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> ('a * 'b * 'c * 'd) input
   14.51 -
   14.52 -  val xml_of_quintuple: 'a output -> 'b output -> 'c output -> 'd output -> 'e output -> ('a * 'b * 'c * 'd * 'e) output
   14.53 -  val quintuple_of_xml: 'a input -> 'b input -> 'c input -> 'd input -> 'e input -> ('a * 'b * 'c * 'd * 'e) input
   14.54 -
   14.55 -  val wrap : string -> 'a output -> 'a output
   14.56 -  val unwrap : ('a -> 'b) -> 'a input -> 'b input
   14.57 -  val wrap_empty : string output
   14.58 -  val unwrap_empty : 'a -> 'a input
   14.59 -  val name_of_wrap : XML.tree -> string
   14.60 -
   14.61 -  val write_to_file: 'a output -> string -> 'a -> unit
   14.62 -  val read_from_file: 'a input -> string -> 'a
   14.63 -
   14.64 -  val serialize_to_file : 'a output -> string -> 'a -> unit
   14.65 -  val deserialize_from_file : 'a input -> string -> 'a
   14.66 -end;
   14.67 -
   14.68 -structure XMLConv : XML_CONV =
   14.69 -struct
   14.70 -  
   14.71 -type 'a input = XML.tree -> 'a
   14.72 -type 'a output = 'a -> XML.tree
   14.73 -exception ParseException of string
   14.74 -
   14.75 -fun parse_err s = raise ParseException s
   14.76 -
   14.77 -fun xml_of_class name = XML.Elem ("class", [("name", name)], []);
   14.78 -
   14.79 -fun class_of_xml (XML.Elem ("class", [("name", name)], [])) = name
   14.80 -  | class_of_xml _ = parse_err "class"
   14.81 - 
   14.82 -fun xml_of_typ (TVar ((s, i), S)) = XML.Elem ("TVar",
   14.83 -      ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
   14.84 -      map xml_of_class S)
   14.85 -  | xml_of_typ (TFree (s, S)) =
   14.86 -      XML.Elem ("TFree", [("name", s)], map xml_of_class S)
   14.87 -  | xml_of_typ (Type (s, Ts)) =
   14.88 -      XML.Elem ("Type", [("name", s)], map xml_of_typ Ts);
   14.89 -
   14.90 -fun intofstr s i = 
   14.91 -    case Int.fromString i of 
   14.92 -        NONE => parse_err (s^", invalid index: "^i)
   14.93 -      | SOME i => i
   14.94 -
   14.95 -fun typ_of_xml (XML.Elem ("TVar", [("name", s)], cs)) = TVar ((s,0), map class_of_xml cs)
   14.96 -  | typ_of_xml (XML.Elem ("TVar", [("name", s), ("index", i)], cs)) = 
   14.97 -    TVar ((s, intofstr "TVar" i), map class_of_xml cs)
   14.98 -  | typ_of_xml (XML.Elem ("TFree", [("name", s)], cs)) = TFree (s, map class_of_xml cs)
   14.99 -  | typ_of_xml (XML.Elem ("Type", [("name", s)], ts)) = Type (s, map typ_of_xml ts)
  14.100 -  | typ_of_xml _ = parse_err "type"
  14.101 -
  14.102 -fun xml_of_term (Bound i) =
  14.103 -      XML.Elem ("Bound", [("index", string_of_int i)], [])
  14.104 -  | xml_of_term (Free (s, T)) =
  14.105 -      XML.Elem ("Free", [("name", s)], [xml_of_typ T])
  14.106 -  | xml_of_term (Var ((s, i), T)) = XML.Elem ("Var",
  14.107 -      ("name", s) :: (if i=0 then [] else [("index", string_of_int i)]),
  14.108 -      [xml_of_typ T])
  14.109 -  | xml_of_term (Const (s, T)) =
  14.110 -      XML.Elem ("Const", [("name", s)], [xml_of_typ T])
  14.111 -  | xml_of_term (t $ u) =
  14.112 -      XML.Elem ("App", [], [xml_of_term t, xml_of_term u])
  14.113 -  | xml_of_term (Abs (s, T, t)) =
  14.114 -      XML.Elem ("Abs", [("vname", s)], [xml_of_typ T, xml_of_term t]);
  14.115 -
  14.116 -fun term_of_xml (XML.Elem ("Bound", [("index", i)], [])) = Bound (intofstr "Bound" i)
  14.117 -  | term_of_xml (XML.Elem ("Free", [("name", s)], [T])) = Free (s, typ_of_xml T)
  14.118 -  | term_of_xml (XML.Elem ("Var",[("name", s)], [T])) = Var ((s,0), typ_of_xml T)
  14.119 -  | term_of_xml (XML.Elem ("Var",[("name", s), ("index", i)], [T])) = Var ((s,intofstr "Var" i), typ_of_xml T)
  14.120 -  | term_of_xml (XML.Elem ("Const", [("name", s)], [T])) = Const (s, typ_of_xml T)
  14.121 -  | term_of_xml (XML.Elem ("App", [], [t, u])) = (term_of_xml t) $ (term_of_xml u)
  14.122 -  | term_of_xml (XML.Elem ("Abs", [("vname", s)], [T, t])) = Abs (s, typ_of_xml T, term_of_xml t)
  14.123 -  | term_of_xml _ = parse_err "term"
  14.124 -
  14.125 -fun xml_of_opttypes NONE = []
  14.126 -  | xml_of_opttypes (SOME Ts) = [XML.Elem ("types", [], map xml_of_typ Ts)];
  14.127 -
  14.128 -(* FIXME: the t argument of PThm and PAxm is actually redundant, since *)
  14.129 -(* it can be looked up in the theorem database. Thus, it could be      *)
  14.130 -(* omitted from the xml representation.                                *)
  14.131 -
  14.132 -fun xml_of_proof (PBound i) =
  14.133 -      XML.Elem ("PBound", [("index", string_of_int i)], [])
  14.134 -  | xml_of_proof (Abst (s, optT, prf)) =
  14.135 -      XML.Elem ("Abst", [("vname", s)],
  14.136 -        (case optT of NONE => [] | SOME T => [xml_of_typ T]) @
  14.137 -        [xml_of_proof prf])
  14.138 -  | xml_of_proof (AbsP (s, optt, prf)) =
  14.139 -      XML.Elem ("AbsP", [("vname", s)],
  14.140 -        (case optt of NONE => [] | SOME t => [xml_of_term t]) @
  14.141 -        [xml_of_proof prf])
  14.142 -  | xml_of_proof (prf % optt) =
  14.143 -      XML.Elem ("Appt", [],
  14.144 -        xml_of_proof prf ::
  14.145 -        (case optt of NONE => [] | SOME t => [xml_of_term t]))
  14.146 -  | xml_of_proof (prf %% prf') =
  14.147 -      XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
  14.148 -  | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
  14.149 -  | xml_of_proof (PThm (_, ((s, t, optTs), _))) =
  14.150 -      XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
  14.151 -  | xml_of_proof (PAxm (s, t, optTs)) =
  14.152 -      XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
  14.153 -  | xml_of_proof (Oracle (s, t, optTs)) =
  14.154 -      XML.Elem ("Oracle", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
  14.155 -  | xml_of_proof MinProof = XML.Elem ("MinProof", [], []);
  14.156 -
  14.157 -fun xml_of_bool b = XML.Elem ("bool", [("value", if b then "true" else "false")], [])
  14.158 -fun xml_of_int i = XML.Elem ("int", [("value", string_of_int i)], [])
  14.159 -fun xml_of_string s = XML.Elem ("string", [("value", s)], [])
  14.160 -fun xml_of_unit () = XML.Elem ("unit", [], [])
  14.161 -fun xml_of_list output ls = XML.Elem ("list", [], map output ls)
  14.162 -fun xml_of_tuple output ls = XML.Elem ("tuple", [], map output ls)
  14.163 -fun xml_of_option output opt = XML.Elem ("option", [], case opt of NONE => [] | SOME x => [output x])
  14.164 -fun wrap s output x = XML.Elem (s, [], [output x])
  14.165 -fun wrap_empty s = XML.Elem (s, [], [])
  14.166 -fun xml_of_pair output1 output2 (x1, x2) = XML.Elem ("pair", [], [output1 x1, output2 x2])
  14.167 -fun xml_of_triple output1 output2 output3 (x1, x2, x3) = XML.Elem ("triple", [], [output1 x1, output2 x2, output3 x3])
  14.168 -fun xml_of_quadruple output1 output2 output3 output4 (x1, x2, x3, x4) = 
  14.169 -    XML.Elem ("quadruple", [], [output1 x1, output2 x2, output3 x3, output4 x4])
  14.170 -fun xml_of_quintuple output1 output2 output3 output4 output5 (x1, x2, x3, x4, x5) = 
  14.171 -    XML.Elem ("quintuple", [], [output1 x1, output2 x2, output3 x3, output4 x4, output5 x5])
  14.172 -                                                                                  
  14.173 -fun bool_of_xml (XML.Elem ("bool", [("value", "true")], [])) = true
  14.174 -  | bool_of_xml (XML.Elem ("bool", [("value", "false")], [])) = false
  14.175 -  | bool_of_xml _ = parse_err "bool"
  14.176 -
  14.177 -fun int_of_xml (XML.Elem ("int", [("value", i)], [])) = intofstr "int" i
  14.178 -  | int_of_xml _ = parse_err "int"
  14.179 -
  14.180 -fun unit_of_xml (XML.Elem ("unit", [], [])) = ()
  14.181 -  | unit_of_xml _ = parse_err "unit"
  14.182 -
  14.183 -fun list_of_xml input (XML.Elem ("list", [], ls)) = map input ls
  14.184 -  | list_of_xml _ _ = parse_err "list"
  14.185 -
  14.186 -fun tuple_of_xml input i (XML.Elem ("tuple", [], ls)) = 
  14.187 -    if i = length ls then map input ls else parse_err "tuple"
  14.188 -  | tuple_of_xml _ _ _ = parse_err "tuple"
  14.189 -
  14.190 -fun option_of_xml input (XML.Elem ("option", [], [])) = NONE
  14.191 -  | option_of_xml input (XML.Elem ("option", [], [opt])) = SOME (input opt)
  14.192 -  | option_of_xml _ _ = parse_err "option"
  14.193 -
  14.194 -fun pair_of_xml input1 input2 (XML.Elem ("pair", [], [x1, x2])) = (input1 x1, input2 x2)
  14.195 -  | pair_of_xml _ _ _ = parse_err "pair"
  14.196 -
  14.197 -fun triple_of_xml input1 input2 input3 (XML.Elem ("triple", [], [x1, x2, x3])) = (input1 x1, input2 x2, input3 x3)
  14.198 -  | triple_of_xml _ _ _ _ = parse_err "triple"
  14.199 -
  14.200 -fun quadruple_of_xml input1 input2 input3 input4 (XML.Elem ("quadruple", [], [x1, x2, x3, x4])) = 
  14.201 -    (input1 x1, input2 x2, input3 x3, input4 x4)
  14.202 -  | quadruple_of_xml _ _ _ _ _ = parse_err "quadruple"
  14.203 -
  14.204 -fun quintuple_of_xml input1 input2 input3 input4 input5 (XML.Elem ("quintuple", [], [x1, x2, x3, x4, x5])) = 
  14.205 -    (input1 x1, input2 x2, input3 x3, input4 x4, input5 x5)
  14.206 -  | quintuple_of_xml _ _ _ _ _ _ = parse_err "quintuple"
  14.207 -
  14.208 -fun unwrap f input (XML.Elem (_, [], [x])) = f (input x)
  14.209 -  | unwrap _ _ _  = parse_err "unwrap"
  14.210 -
  14.211 -fun unwrap_empty x (XML.Elem (_, [], [])) = x 
  14.212 -  | unwrap_empty _ _ = parse_err "unwrap_unit"
  14.213 -
  14.214 -fun name_of_wrap (XML.Elem (name, _, _)) = name
  14.215 -  | name_of_wrap _ = parse_err "name_of_wrap"
  14.216 -
  14.217 -fun string_of_xml (XML.Elem ("string", [("value", s)], [])) = s
  14.218 -  | string_of_xml _ = parse_err "string"
  14.219 -
  14.220 -fun xml_of_mixfix NoSyn = wrap_empty "nosyn"
  14.221 -  | xml_of_mixfix Structure = wrap_empty "structure"
  14.222 -  | xml_of_mixfix (Mixfix args) = wrap "mixfix" (xml_of_triple xml_of_string (xml_of_list xml_of_int) xml_of_int) args
  14.223 -  | xml_of_mixfix (Delimfix s) = wrap "delimfix" xml_of_string s
  14.224 -  | xml_of_mixfix (Infix args) = wrap "infix" (xml_of_pair xml_of_string xml_of_int) args
  14.225 -  | xml_of_mixfix (Infixl args) = wrap "infixl" (xml_of_pair xml_of_string xml_of_int) args
  14.226 -  | xml_of_mixfix (Infixr args) = wrap "infixr" (xml_of_pair xml_of_string xml_of_int) args
  14.227 -  | xml_of_mixfix (Binder args) = wrap "binder" (xml_of_triple xml_of_string xml_of_int xml_of_int) args
  14.228 -                                  
  14.229 -fun mixfix_of_xml e = 
  14.230 -    (case name_of_wrap e of 
  14.231 -         "nosyn" => unwrap_empty NoSyn 
  14.232 -       | "structure" => unwrap_empty Structure 
  14.233 -       | "mixfix" => unwrap Mixfix (triple_of_xml string_of_xml (list_of_xml int_of_xml) int_of_xml)
  14.234 -       | "delimfix" => unwrap Delimfix string_of_xml
  14.235 -       | "infix" => unwrap Infix (pair_of_xml string_of_xml int_of_xml) 
  14.236 -       | "infixl" => unwrap Infixl (pair_of_xml string_of_xml int_of_xml)  
  14.237 -       | "infixr" => unwrap Infixr (pair_of_xml string_of_xml int_of_xml)
  14.238 -       | "binder" => unwrap Binder (triple_of_xml string_of_xml int_of_xml int_of_xml)
  14.239 -       | _ => parse_err "mixfix"
  14.240 -    ) e
  14.241 -
  14.242 -
  14.243 -fun to_file f output fname x = File.write (Path.explode fname) (f (output x))
  14.244 - 
  14.245 -fun from_file f input fname = 
  14.246 -    let
  14.247 -        val _ = writeln "read_from_file enter"
  14.248 -        val s = File.read (Path.explode fname)
  14.249 -        val _ = writeln "done: read file"
  14.250 -        val tree = timeit (fn () => f s)
  14.251 -        val _ = writeln "done: tree"
  14.252 -        val x = timeit (fn () => input tree)
  14.253 -        val _ = writeln "done: input"
  14.254 -    in
  14.255 -        x
  14.256 -    end
  14.257 -
  14.258 -fun write_to_file x = to_file XML.string_of_tree x
  14.259 -fun read_from_file x = timeit (fn () => (writeln "read_from_file"; from_file XML.tree_of_string x))
  14.260 -
  14.261 -fun serialize_to_file x = to_file XML.encoded_string_of_tree x
  14.262 -fun deserialize_from_file x = timeit (fn () => (writeln "deserialize_from_file"; from_file XML.tree_of_encoded_string x))
  14.263 -
  14.264 -end;
  14.265 -
  14.266 -structure XMLConvOutput =
  14.267 -struct
  14.268 -open XMLConv
  14.269 - 
  14.270 -val typ = xml_of_typ
  14.271 -val term = xml_of_term
  14.272 -val mixfix = xml_of_mixfix
  14.273 -val proof = xml_of_proof
  14.274 -val bool = xml_of_bool
  14.275 -val int = xml_of_int
  14.276 -val string = xml_of_string
  14.277 -val unit = xml_of_unit
  14.278 -val list = xml_of_list
  14.279 -val pair = xml_of_pair
  14.280 -val option = xml_of_option
  14.281 -val triple = xml_of_triple
  14.282 -val quadruple = xml_of_quadruple
  14.283 -val quintuple = xml_of_quintuple
  14.284 -
  14.285 -end
  14.286 -
  14.287 -structure XMLConvInput = 
  14.288 -struct
  14.289 -open XMLConv
  14.290 -
  14.291 -val typ = typ_of_xml
  14.292 -val term = term_of_xml
  14.293 -val mixfix = mixfix_of_xml
  14.294 -val bool = bool_of_xml
  14.295 -val int = int_of_xml
  14.296 -val string = string_of_xml
  14.297 -val unit = unit_of_xml
  14.298 -val list = list_of_xml
  14.299 -val pair = pair_of_xml
  14.300 -val option = option_of_xml
  14.301 -val triple = triple_of_xml
  14.302 -val quadruple = quadruple_of_xml
  14.303 -val quintuple = quintuple_of_xml
  14.304 -
  14.305 -end
  14.306 -
    15.1 --- a/src/HOL/IsaMakefile	Wed Jul 20 08:46:17 2011 +0200
    15.2 +++ b/src/HOL/IsaMakefile	Wed Jul 20 10:11:08 2011 +0200
    15.3 @@ -555,13 +555,11 @@
    15.4  ## HOL-Import
    15.5  
    15.6  IMPORTER_FILES = \
    15.7 -  Import/ImportRecorder.thy Import/HOL4Compat.thy \
    15.8 +  Import/HOL4Compat.thy \
    15.9    Import/HOLLightCompat.thy Import/HOL4Setup.thy Import/HOL4Syntax.thy \
   15.10    Import/MakeEqual.thy Import/ROOT.ML Import/hol4rews.ML \
   15.11 -  Import/import.ML Import/importrecorder.ML Import/import_syntax.ML \
   15.12 -  Import/lazy_seq.ML Import/mono_scan.ML Import/mono_seq.ML \
   15.13 -  Import/proof_kernel.ML Import/replay.ML Import/scan.ML Import/seq.ML \
   15.14 -  Import/shuffler.ML Import/xml.ML Import/xmlconv.ML \
   15.15 +  Import/import.ML Import/import_syntax.ML \
   15.16 +  Import/proof_kernel.ML Import/replay.ML Import/shuffler.ML \
   15.17    Library/ContNotDenum.thy Old_Number_Theory/Primes.thy
   15.18  
   15.19  HOL-Import: HOL $(LOG)/HOL-Import.gz