# HG changeset patch # User huffman # Date 1232039442 28800 # Node ID 2de73447d47ca05a80747b9370f223777bf856cf # Parent 08824fad8879d467c92e18664749f6e30b63addf# Parent 8fd3c1c7f0cb6391b747051cacbe87779550d784 merged. diff -r 08824fad8879 -r 2de73447d47c src/FOL/ex/LocaleTest.thy --- a/src/FOL/ex/LocaleTest.thy Thu Jan 15 08:11:50 2009 -0800 +++ b/src/FOL/ex/LocaleTest.thy Thu Jan 15 09:10:42 2009 -0800 @@ -1,7 +1,7 @@ (* Title: FOL/ex/NewLocaleTest.thy Author: Clemens Ballarin, TU Muenchen -Testing environment for locale expressions --- experimental. +Testing environment for locale expressions. *) theory LocaleTest @@ -483,4 +483,6 @@ thm local_free.lone [where ?zero = 0] qed +ML_val {* reset Toplevel.debug *} + end diff -r 08824fad8879 -r 2de73447d47c src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Thu Jan 15 08:11:50 2009 -0800 +++ b/src/HOL/Library/LaTeXsugar.thy Thu Jan 15 09:10:42 2009 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/Library/LaTeXsugar.thy - ID: $Id$ Author: Gerwin Klain, Tobias Nipkow, Norbert Schirmer Copyright 2005 NICTA and TUM *) diff -r 08824fad8879 -r 2de73447d47c src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Thu Jan 15 08:11:50 2009 -0800 +++ b/src/HOL/Library/OptionalSugar.thy Thu Jan 15 09:10:42 2009 -0800 @@ -1,5 +1,4 @@ (* Title: HOL/Library/OptionalSugar.thy - ID: $Id$ Author: Gerwin Klain, Tobias Nipkow Copyright 2005 NICTA and TUM *) @@ -37,6 +36,36 @@ "_bind (p#DUMMY) e" <= "_bind p (hd e)" "_bind (DUMMY#p) e" <= "_bind p (tl e)" +(* type constraints with spacing *) +setup {* +let + val typ = SimpleSyntax.read_typ; + val typeT = Syntax.typeT; + val spropT = Syntax.spropT; +in + Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ + ("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\_", [4, 0], 3))] + #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ + ("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), + ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \ _", [4, 0], 3))] +end +*} + +(* sorts as intersections *) +setup {* +let + val sortT = Type ("sort", []); (*FIXME*) + val classesT = Type ("classes", []); (*FIXME*) +in + Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ + ("_topsort", sortT, Mixfix ("\", [], Syntax.max_pri)), + ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)), + ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \ _", [], Syntax.max_pri)), + ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \ _", [], Syntax.max_pri)) + ] +end +*} end (*>*) diff -r 08824fad8879 -r 2de73447d47c src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Thu Jan 15 08:11:50 2009 -0800 +++ b/src/HOL/Tools/function_package/size.ML Thu Jan 15 09:10:42 2009 -0800 @@ -1,6 +1,5 @@ (* Title: HOL/Tools/function_package/size.ML - ID: $Id$ - Author: Stefan Berghofer, Florian Haftmann, TU Muenchen + Author: Stefan Berghofer, Florian Haftmann & Alexander Krauss, TU Muenchen Size functions for datatypes. *) @@ -81,7 +80,7 @@ val param_size = AList.lookup op = param_size_fs; val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |> - List.mapPartial (Option.map snd o lookup_size thy) |> flat; + map_filter (Option.map snd o lookup_size thy) |> flat; val extra_size = Option.map fst o lookup_size thy; val (((size_names, size_fns), def_names), def_names') = @@ -180,7 +179,7 @@ let val Ts = map (typ_of_dtyp descr sorts) cargs; val tnames = Name.variant_list f_names (DatatypeProp.make_tnames Ts); - val ts = List.mapPartial (fn (sT as (s, T), dt) => + val ts = map_filter (fn (sT as (s, T), dt) => Option.map (fn sz => sz $ Free sT) (if p dt then size_of_type size_of extra_size size_ofp T else NONE)) (tnames ~~ Ts ~~ cargs) diff -r 08824fad8879 -r 2de73447d47c src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Thu Jan 15 08:11:50 2009 -0800 +++ b/src/Pure/General/markup.ML Thu Jan 15 09:10:42 2009 -0800 @@ -91,6 +91,8 @@ val failedN: string val failed: T val finishedN: string val finished: T val disposedN: string val disposed: T + val editsN: string val edits: string -> T + val editN: string val edit: string -> string -> T val pidN: string val sessionN: string val classN: string @@ -269,6 +271,14 @@ val (disposedN, disposed) = markup_elem "disposed"; +(* interactive documents *) + +val (editsN, edits) = markup_string "edits" idN; + +val editN = "edit"; +fun edit id state_id : T = (editN, [(idN, id), (stateN, state_id)]); + + (* messages *) val pidN = "pid"; diff -r 08824fad8879 -r 2de73447d47c src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Thu Jan 15 08:11:50 2009 -0800 +++ b/src/Pure/General/markup.scala Thu Jan 15 09:10:42 2009 -0800 @@ -119,6 +119,12 @@ val DISPOSED = "disposed" + /* interactive documents */ + + val EDITS = "edits" + val EDIT = "edit" + + /* messages */ val PID = "pid" diff -r 08824fad8879 -r 2de73447d47c src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Jan 15 08:11:50 2009 -0800 +++ b/src/Pure/Isar/expression.ML Thu Jan 15 09:10:42 2009 -0800 @@ -26,6 +26,8 @@ (* Interpretation *) val cert_goal_expression: expression_i -> Proof.context -> (term list list * (string * morphism) list * morphism) * Proof.context; + val read_goal_expression: expression -> Proof.context -> + (term list list * (string * morphism) list * morphism) * Proof.context; val sublocale: string -> expression_i -> theory -> Proof.state; val sublocale_cmd: string -> expression -> theory -> Proof.state; @@ -812,21 +814,17 @@ local -datatype goal = Reg of string * Morphism.morphism | Eqns of Attrib.binding list; - fun gen_interpretation prep_expr parse_prop prep_attr - expression equations thy = + expression equations theory = let - val ctxt = ProofContext.init thy; - - val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt; + val ((propss, regs, export), expr_ctxt) = ProofContext.init theory + |> prep_expr expression; val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt; - val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations; + val eq_attns = map ((apsnd o map) (prep_attr theory) o fst) equations; val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; - (*** alternative code -- unclear why it does not work yet ***) fun store_reg ((name, morph), thms) thy = let val thms' = map (Element.morph_witness export') thms; @@ -841,7 +839,7 @@ thy |> fold (fn (name, morph) => Locale.activate_global_facts (name, morph $> export)) regs - | store_eqns_activate regs thms thys = + | store_eqns_activate regs thms thy = let val thms' = thms |> map (Element.conclude_witness #> Morphism.thm (export' $> export) #> @@ -866,40 +864,7 @@ in ProofContext.theory (fold_map store_reg (regs ~~ wits_reg) #-> (fn regs => store_eqns_activate regs wits_eq)) end; - (*** alternative code end ***) - fun store (Reg (name, morph), thms) (regs, thy) = - let - val thms' = map (Element.morph_witness export') thms; - val morph' = morph $> Element.satisfy_morphism thms'; - val add = Locale.add_registration (name, (morph', export)); - in ((name, morph') :: regs, add thy) end - | store (Eqns [], []) (regs, thy) = - let val add = fold_rev (fn (name, morph) => - Locale.activate_global_facts (name, morph $> export)) regs; - in (regs, add thy) end - | store (Eqns attns, thms) (regs, thy) = - let - val thms' = thms |> map (Element.conclude_witness #> - Morphism.thm (export' $> export) #> - LocalDefs.meta_rewrite_rule (ProofContext.init thy) #> - Drule.abs_def); - val eq_morph = - Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $> - Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms'); - val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns; - val add = - fold_rev (fn (name, morph) => - Locale.amend_registration eq_morph (name, morph) #> - Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs #> - PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #> - snd - in (regs, add thy) end; - - fun after_qed results = - ProofContext.theory (fn thy => - fold store (map Reg regs @ [Eqns eq_attns] ~~ - prep_result (propss @ [eqns]) results) ([], thy) |> snd); in goal_ctxt |> Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |> diff -r 08824fad8879 -r 2de73447d47c src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Thu Jan 15 08:11:50 2009 -0800 +++ b/src/Pure/Isar/isar_document.ML Thu Jan 15 09:10:42 2009 -0800 @@ -18,12 +18,11 @@ structure IsarDocument: ISAR_DOCUMENT = struct - (* unique identifiers *) -type document_id = string; +type state_id = string; type command_id = string; -type state_id = string; +type document_id = string; fun new_id () = "isabelle:" ^ serial_string (); @@ -31,59 +30,13 @@ fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id); -(** execution states **) - -(* command status *) - -datatype status = - Unprocessed | - Running of Toplevel.state option future | - Failed | - Finished of Toplevel.state; - -fun markup_status Unprocessed = Markup.unprocessed - | markup_status (Running future) = Markup.running (Task_Queue.str_of_task (Future.task_of future)) - | markup_status Failed = Markup.failed - | markup_status (Finished _) = Markup.finished; - -fun update_status retry tr state status = - (case status of - Unprocessed => SOME (Running (Future.fork_pri 1 (fn () => - (case Toplevel.transition true tr state of - NONE => (Toplevel.error_msg tr (ERROR "Cannot terminate here!", ""); NONE) - | SOME (_, SOME err) => (Toplevel.error_msg tr err; NONE) - | SOME (state', NONE) => SOME state')))) - | Running future => - (case Future.peek future of - NONE => NONE - | SOME (Exn.Result NONE) => SOME Failed - | SOME (Exn.Result (SOME state')) => SOME (Finished state') - | SOME (Exn.Exn exn) => (Toplevel.error_msg tr (exn, ""); SOME Failed)) - | Failed => if retry then SOME Unprocessed else NONE - | _ => NONE); - - -(* state *) - -datatype state = State of - {prev: state_id option, - command: command_id, - status: status}; - -fun make_state prev command status = State {prev = prev, command = command, status = status}; - - (** documents **) (* command entries *) -datatype entry = Entry of - {prev: command_id option, - next: command_id option, - state: state_id option}; - -fun make_entry prev next state = Entry {prev = prev, next = next, state = state}; +datatype entry = Entry of {next: command_id option, state: state_id option}; +fun make_entry next state = Entry {next = next, state = state}; fun the_entry entries (id: command_id) = (case Symtab.lookup entries id of @@ -92,11 +45,13 @@ fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry); -fun map_entry (id: command_id) f entries = - let - val {prev, next, state} = the_entry entries id; - val (prev', next', state') = f (prev, next, state); - in put_entry (id, make_entry prev' next' state') entries end; +fun put_entry_state (id: command_id) state entries = + let val {next, ...} = the_entry entries id + in put_entry (id, make_entry next state) entries end; + +fun reset_entry_state id = put_entry_state id NONE; +fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id); + (* document *) @@ -114,7 +69,7 @@ make_document dir name start (f entries); -(* iterating entries *) +(* iterate entries *) fun fold_entries opt_id f (Document {start, entries, ...}) = let @@ -122,40 +77,33 @@ | apply (SOME id) x = apply (#next (the_entry entries id)) (f id x); in if is_some opt_id then apply opt_id else apply (SOME start) end; -fun get_first_entries opt_id f (Document {start, entries, ...}) = +fun find_entries P (Document {start, entries, ...}) = let - fun get NONE = NONE - | get (SOME id) = (case f id of NONE => get (#next (the_entry entries id)) | some => some); - in if is_some opt_id then get opt_id else get (SOME start) end; - -fun find_first_entries opt_id P = - get_first_entries opt_id (fn x => if P x then SOME x else NONE); + fun find _ NONE = NONE + | find prev (SOME id) = + if P id then SOME (prev, id) + else find (SOME id) (#next (the_entry entries id)); + in find NONE (SOME start) end; (* modify entries *) -fun insert_entry (id: command_id, id2: command_id) = map_entries (fn entries => - let val {prev, next, state} = the_entry entries id in - entries |> - (case next of - NONE => put_entry (id2, make_entry (SOME id) NONE NONE) - | SOME id3 => - put_entry (id, make_entry prev (SOME id2) state) #> - put_entry (id2, make_entry (SOME id) (SOME id3) NONE) #> - put_entry (id3, make_entry (SOME id2) (#next (the_entry entries id3)) NONE)) +fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries => + let val {next, state} = the_entry entries id in + entries + |> put_entry (id, make_entry (SOME id2) state) + |> put_entry (id2, make_entry next NONE) end); fun delete_after (id: command_id) = map_entries (fn entries => - let val {prev, next, state} = the_entry entries id in - entries |> - (case next of - NONE => error ("Missing next entry: " ^ quote id) - | SOME id2 => + let val {next, state} = the_entry entries id in + (case next of + NONE => error ("No next entry to delete: " ^ quote id) + | SOME id2 => + entries |> (case #next (the_entry entries id2) of - NONE => put_entry (id, make_entry prev NONE state) - | SOME id3 => - put_entry (id, make_entry prev (SOME id3) state) #> - put_entry (id3, make_entry (SOME id) (#next (the_entry entries id3)) NONE))) + NONE => put_entry (id, make_entry NONE state) + | SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3)) end); @@ -163,7 +111,7 @@ (** global configuration **) local - val global_states = ref (Symtab.empty: state Symtab.table); + val global_states = ref (Symtab.empty: Toplevel.state option future Symtab.table); val global_commands = ref (Symtab.empty: Toplevel.transition Symtab.table); val global_documents = ref (Symtab.empty: document Symtab.table); in @@ -192,12 +140,12 @@ fun the_state (id: state_id) = (case Symtab.lookup (get_states ()) id of NONE => err_undef "state" id - | SOME (State state) => state); + | SOME state => state); fun define_command id tr = change_commands (Symtab.update_new (id, Toplevel.put_id id tr)) - handle Symtab.DUP dup => err_dup ("command " ^ Toplevel.name_of tr) dup; + handle Symtab.DUP dup => err_dup "command" dup; fun the_command (id: command_id) = (case Symtab.lookup (get_commands ()) id of @@ -221,8 +169,8 @@ let val (dir, name) = ThyLoad.split_thy_path path; val _ = define_command id Toplevel.empty; - val _ = define_state id (make_state NONE id (Finished Toplevel.toplevel)); - val entries = Symtab.make [(id, make_entry NONE NONE (SOME id))]; + val _ = define_state id (Future.value (SOME Toplevel.toplevel)); + val entries = Symtab.make [(id, make_entry NONE (SOME id))]; val _ = define_document id (make_document dir name id entries); in () end; @@ -231,7 +179,10 @@ (* document editing *) -fun refresh_states old_document new_document = +fun update_state tr state = Future.fork_deps [state] (fn () => + (case Future.join state of NONE => NONE | SOME st => Toplevel.run_command tr st)); + +fun update_states old_document new_document = let val Document {entries = old_entries, ...} = old_document; val Document {entries = new_entries, ...} = new_document; @@ -243,37 +194,42 @@ fun cancel_state id () = (case the_entry old_entries id of - {state = SOME state_id, ...} => - (case the_state state_id of - {status = Running future, ...} => Future.cancel future - | _ => ()) + {state = SOME state_id, ...} => Future.cancel (the_state state_id) | _ => ()); - fun new_state id (prev_state_id, new_states) = + fun new_state id (state_id, updates) = let - val state_id = new_id (); - val state = make_state prev_state_id id Unprocessed; - val _ = define_state state_id state; - in (SOME state_id, (state_id, state) :: new_states) end; + val state_id' = new_id (); + val state' = update_state (the_command id) (the_state state_id); + val _ = define_state state_id' state'; + in (state_id', (id, state_id') :: updates) end; in - (case find_first_entries NONE is_changed old_document of - NONE => new_document - | SOME id => + (case find_entries is_changed old_document of + NONE => ([], new_document) + | SOME (prev, id) => let val _ = fold_entries (SOME id) cancel_state old_document (); - val (_, new_states) = fold_entries (SOME id) new_state new_document (NONE, []); - (* FIXME update states *) - in new_document end) + val prev_state_id = the (#state (the_entry new_entries (the prev))); + val (_, updates) = fold_entries (SOME id) new_state new_document (prev_state_id, []); + val new_document' = new_document |> map_entries (fold set_entry_state updates); + in (updates, new_document') end) end; +fun report_updates _ [] = () + | report_updates (document_id: document_id) updates = + implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates) + |> Markup.markup (Markup.edits document_id) + |> Output.status; + fun edit_document (id: document_id) (id': document_id) edits = let val document = Document (the_document id); - val document' = + val (updates, document') = document - |> fold (fn (id, SOME id2) => insert_entry (id, id2) | (id, NONE) => delete_after id) edits - |> refresh_states document; + |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits + |> update_states document; val _ = define_document id' document'; + val _ = report_updates id' updates; in () end; @@ -300,7 +256,7 @@ val _ = OuterSyntax.internal_command "Isar.edit_document" (P.string -- P.string -- V.list (P.string -- (P.string >> SOME) || P.string >> rpair NONE) - >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => end_document id new_id edits))); + >> (fn ((id, new_id), edits) => Toplevel.imperative (fn () => edit_document id new_id edits))); end; diff -r 08824fad8879 -r 2de73447d47c src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Jan 15 08:11:50 2009 -0800 +++ b/src/Pure/Isar/toplevel.ML Thu Jan 15 09:10:42 2009 -0800 @@ -96,6 +96,7 @@ val transition: bool -> transition -> state -> (state * (exn * string) option) option val commit_exit: Position.T -> transition val command: transition -> state -> state + val run_command: transition -> state -> state option val excursion: (transition * transition list) list -> (transition * state) list lazy end; @@ -693,6 +694,16 @@ | SOME (_, SOME exn_info) => raise EXCURSION_FAIL exn_info | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); +fun command_result tr st = + let val st' = command tr st + in (st', st') end; + +fun run_command tr st = + (case transition true tr st of + SOME (st', NONE) => (status tr Markup.finished; SOME st') + | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE) + | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE)); + (* excursion of units, consisting of commands with proof *) @@ -702,10 +713,6 @@ fun init _ = NONE; ); -fun command_result tr st = - let val st' = command tr st - in (st', st') end; - fun proof_result immediate (tr, proof_trs) st = let val st' = command tr st in if immediate orelse null proof_trs orelse diff -r 08824fad8879 -r 2de73447d47c src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Thu Jan 15 08:11:50 2009 -0800 +++ b/src/Pure/Thy/present.ML Thu Jan 15 09:10:42 2009 -0800 @@ -467,7 +467,7 @@ val _ = add_file (Path.append html_prefix base_html, HTML.ml_file (Url.File base) (File.read path)); in (Url.File base_html, Url.File raw_path, loadit) end - | NONE => error ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path))); + | NONE => error ("Browser info: expected to find ML file " ^ quote (Path.implode raw_path))); val files_html = map prep_file files; diff -r 08824fad8879 -r 2de73447d47c src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Thu Jan 15 08:11:50 2009 -0800 +++ b/src/Pure/Thy/thy_output.ML Thu Jan 15 09:10:42 2009 -0800 @@ -11,6 +11,7 @@ val quotes: bool ref val indent: int ref val source: bool ref + val break: bool ref val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit val defined_command: string -> bool