merged.
--- 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
--- 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
*)
--- 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 ("_\<Colon>_", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
+ #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
+ ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [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 ("\<top>", [], Syntax.max_pri)),
+ ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
+ ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
+ ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
+ ]
+end
+*}
end
(*>*)
--- 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)
--- 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";
--- 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"
--- 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])) |>
--- 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;
--- 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
--- 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;
--- 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