| author | huffman |
| Mon, 15 Aug 2011 19:42:52 -0700 | |
| changeset 44220 | e5753e2a5944 |
| parent 44219 | f738e3200e24 (current diff) |
| parent 44204 | 3cdc4176638c (diff) |
| child 44221 | bff7f7afb2db |
--- a/src/HOL/Equiv_Relations.thy Mon Aug 15 18:35:36 2011 -0700 +++ b/src/HOL/Equiv_Relations.thy Mon Aug 15 19:42:52 2011 -0700 @@ -402,8 +402,8 @@ by (erule part_equivpE, erule transpE) lemma part_equivp_typedef: - "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)" - by (auto elim: part_equivpE simp add: mem_def) + "part_equivp R \<Longrightarrow> \<exists>d. d \<in> {c. \<exists>x. R x x \<and> c = Collect (R x)}" + by (auto elim: part_equivpE) text {* Total equivalences *}
--- a/src/HOL/Quotient.thy Mon Aug 15 18:35:36 2011 -0700 +++ b/src/HOL/Quotient.thy Mon Aug 15 19:42:52 2011 -0700 @@ -603,66 +603,52 @@ locale quot_type = fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" - and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" - and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" + and Abs :: "'a set \<Rightarrow> 'b" + and Rep :: "'b \<Rightarrow> 'a set" assumes equivp: "part_equivp R" - and rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x" + and rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = Collect (R x)" and rep_inverse: "\<And>x. Abs (Rep x) = x" - and abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c" + and abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = Collect (R x)))) \<Longrightarrow> (Rep (Abs c)) = c" and rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)" begin definition abs :: "'a \<Rightarrow> 'b" where - "abs x = Abs (R x)" + "abs x = Abs (Collect (R x))" definition rep :: "'b \<Rightarrow> 'a" where - "rep a = Eps (Rep a)" - -lemma homeier5: - assumes a: "R r r" - shows "Rep (Abs (R r)) = R r" - apply (subst abs_inverse) - using a by auto + "rep a = (SOME x. x \<in> Rep a)" -theorem homeier6: - assumes a: "R r r" - and b: "R s s" - shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s" - by (metis a b homeier5) - -theorem homeier8: +lemma some_collect: assumes "R r r" - shows "R (Eps (R r)) = R r" - using assms equivp[simplified part_equivp_def] - apply clarify - by (metis assms exE_some) + shows "R (SOME x. x \<in> Collect (R r)) = R r" + apply simp + by (metis assms exE_some equivp[simplified part_equivp_def]) lemma Quotient: shows "Quotient R abs rep" unfolding Quotient_def abs_def rep_def proof (intro conjI allI) fix a r s - show "Abs (R (Eps (Rep a))) = a" - using [[metis_new_skolemizer = false]] - by (metis equivp exE_some part_equivp_def rep_inverse rep_prop) - show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))" - by (metis homeier6 equivp[simplified part_equivp_def]) - show "R (Eps (Rep a)) (Eps (Rep a))" proof - - obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto - have "R (Eps (R x)) x" using homeier8 r by simp - then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast - then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp - then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp + show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof - + obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto + have "R (SOME x. x \<in> Rep a) x" using r rep some_collect by metis + then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast + then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" + using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`) qed - qed - + have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop) + then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto + have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" + by (metis Collect_def abs_inverse) + then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))" + using equivp[simplified part_equivp_def] by metis + qed end - subsection {* ML setup *} text {* Auxiliary data for the quotient package *}
--- a/src/HOL/Quotient_Examples/FSet.thy Mon Aug 15 18:35:36 2011 -0700 +++ b/src/HOL/Quotient_Examples/FSet.thy Mon Aug 15 19:42:52 2011 -0700 @@ -561,9 +561,9 @@ shows "fset S = fset T \<longleftrightarrow> S = T" by (descending) (simp) -lemma filter_fset [simp]: - shows "fset (filter_fset P xs) = P \<inter> fset xs" - by (descending) (auto simp add: mem_def) +lemma filter_fset [simp]: + shows "fset (filter_fset P xs) = Collect P \<inter> fset xs" + by (descending) (auto) lemma remove_fset [simp]: shows "fset (remove_fset x xs) = fset xs - {x}"
--- a/src/HOL/Tools/Quotient/quotient_typ.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Mon Aug 15 19:42:52 2011 -0700 @@ -48,8 +48,8 @@ (*** definition of quotient types ***) -val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)} -val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)} +val mem_def1 = @{lemma "y : Collect S ==> S y" by simp} +val mem_def2 = @{lemma "S y ==> y : Collect S" by simp} (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *) fun typedef_term rel rty lthy = @@ -58,9 +58,14 @@ [("x", rty), ("c", HOLogic.mk_setT rty)] |> Variable.variant_frees lthy [rel] |> map Free + fun mk_collect T = + Const (@{const_name Collect}, (T --> @{typ bool}) --> HOLogic.mk_setT T) + val collect_in = mk_collect rty + val collect_out = mk_collect (HOLogic.mk_setT rty) in - lambda c (HOLogic.exists_const rty $ - lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x)))) + collect_out $ (lambda c (HOLogic.exists_const rty $ + lambda x (HOLogic.mk_conj (rel $ x $ x, + HOLogic.mk_eq (c, collect_in $ (rel $ x)))))) end
--- a/src/Pure/Concurrent/future.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/Concurrent/future.ML Mon Aug 15 19:42:52 2011 -0700 @@ -39,6 +39,7 @@ val task_of: 'a future -> Task_Queue.task val peek: 'a future -> 'a Exn.result option val is_finished: 'a future -> bool + val get_finished: 'a future -> 'a val interruptible_task: ('a -> 'b) -> 'a -> 'b val cancel_group: Task_Queue.group -> unit val cancel: 'a future -> unit @@ -105,6 +106,11 @@ fun peek x = Single_Assignment.peek (result_of x); fun is_finished x = is_some (peek x); +fun get_finished x = + (case peek x of + SOME res => Exn.release res + | NONE => raise Fail "Unfinished future evaluation"); + (** scheduling **)
--- a/src/Pure/Concurrent/lazy.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/Concurrent/lazy.ML Mon Aug 15 19:42:52 2011 -0700 @@ -10,6 +10,8 @@ sig type 'a lazy val peek: 'a lazy -> 'a Exn.result option + val is_finished: 'a lazy -> bool + val get_finished: 'a lazy -> 'a val lazy: (unit -> 'a) -> 'a lazy val value: 'a -> 'a lazy val force_result: 'a lazy -> 'a Exn.result @@ -36,6 +38,13 @@ fun lazy e = Lazy (Synchronized.var "lazy" (Expr e)); fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a))); +fun is_finished x = is_some (peek x); + +fun get_finished x = + (case peek x of + SOME res => Exn.release res + | NONE => raise Fail "Unfinished lazy evaluation"); + (* force result *)
--- a/src/Pure/Concurrent/lazy_sequential.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/Concurrent/lazy_sequential.ML Mon Aug 15 19:42:52 2011 -0700 @@ -25,6 +25,13 @@ fun lazy e = Lazy (Unsynchronized.ref (Expr e)); fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a))); +fun is_finished x = is_some (peek x); + +fun get_finished x = + (case peek x of + SOME res => Exn.release res + | NONE => raise Fail "Unfinished lazy evaluation"); + (* force result *)
--- a/src/Pure/General/graph.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/General/graph.ML Mon Aug 15 19:42:52 2011 -0700 @@ -35,19 +35,19 @@ val del_nodes: key list -> 'a T -> 'a T (*exception UNDEF*) val del_node: key -> 'a T -> 'a T (*exception UNDEF*) val is_edge: 'a T -> key * key -> bool - val add_edge: key * key -> 'a T -> 'a T - val del_edge: key * key -> 'a T -> 'a T + val add_edge: key * key -> 'a T -> 'a T (*exception UNDEF*) + val del_edge: key * key -> 'a T -> 'a T (*exception UNDEF*) val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*) val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) -> 'a T * 'a T -> 'a T (*exception DUP*) val irreducible_paths: 'a T -> key * key -> key list list val all_paths: 'a T -> key * key -> key list list exception CYCLES of key list list - val add_edge_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*) - val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exception CYCLES*) + val add_edge_acyclic: key * key -> 'a T -> 'a T (*exception UNDEF | CYCLES*) + val add_deps_acyclic: key * key list -> 'a T -> 'a T (*exception UNDEF | CYCLES*) val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) val topological_order: 'a T -> key list - val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*) + val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception UNDEF | CYCLES*) val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*) exception DEP of key * key val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list (*exception DEP*)
--- a/src/Pure/General/position.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/General/position.ML Mon Aug 15 19:42:52 2011 -0700 @@ -18,6 +18,7 @@ val none: T val start: T val file_name: string -> Properties.T + val file_only: string -> T val file: string -> T val line: int -> T val line_file: int -> string -> T @@ -104,6 +105,7 @@ fun file_name "" = [] | file_name name = [(Markup.fileN, name)]; +fun file_only name = Pos ((0, 0, 0), file_name name); fun file name = Pos ((1, 1, 0), file_name name); fun line_file i name = Pos ((i, 1, 0), file_name name);
--- a/src/Pure/General/secure.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/General/secure.ML Mon Aug 15 19:42:52 2011 -0700 @@ -63,7 +63,7 @@ val use_file = Secure.use_file; fun use s = - Position.setmp_thread_data (Position.of_properties (Position.file_name s)) + Position.setmp_thread_data (Position.file_only s) (fn () => Secure.use_file ML_Parse.global_context true s handle ERROR msg => (writeln msg; error "ML error")) ();
--- a/src/Pure/Isar/toplevel.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/Isar/toplevel.ML Mon Aug 15 19:42:52 2011 -0700 @@ -185,8 +185,8 @@ | _ => raise UNDEF); fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy - | end_theory pos (State (NONE, _)) = error ("Missing theory " ^ Position.str_of pos) - | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos); + | end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos) + | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos); (* print state *)
--- a/src/Pure/PIDE/document.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/PIDE/document.ML Mon Aug 15 19:42:52 2011 -0700 @@ -23,7 +23,7 @@ type edit = string * node_edit type state val init_state: state - val get_theory: state -> version_id -> Position.T -> string -> theory + val join_commands: state -> unit val cancel_execution: state -> unit -> unit val define_command: command_id -> string -> state -> state val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state @@ -61,32 +61,34 @@ abstype node = Node of {header: node_header, entries: exec_id option Entries.T, (*command entries with excecutions*) - last: exec_id} (*last entry with main result*) + result: Toplevel.state lazy} and version = Version of node Graph.T (*development graph wrt. static imports*) with -fun make_node (header, entries, last) = - Node {header = header, entries = entries, last = last}; +fun make_node (header, entries, result) = + Node {header = header, entries = entries, result = result}; -fun map_node f (Node {header, entries, last}) = - make_node (f (header, entries, last)); +fun map_node f (Node {header, entries, result}) = + make_node (f (header, entries, result)); fun get_header (Node {header, ...}) = header; -fun set_header header = map_node (fn (_, entries, last) => (header, entries, last)); +fun set_header header = map_node (fn (_, entries, result) => (header, entries, result)); -fun map_entries f (Node {header, entries, last}) = make_node (header, f entries, last); +fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result); fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; -fun get_last (Node {last, ...}) = last; -fun set_last last = map_node (fn (header, entries, _) => (header, entries, last)); +fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result); +fun set_result result = map_node (fn (header, entries, _) => (header, entries, result)); -val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id); -val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id)); +val empty_exec = Lazy.value Toplevel.toplevel; +val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec); +val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec)); fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes; -fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f; +fun default_node name = Graph.default_node (name, empty_node); +fun update_node name f = default_node name #> Graph.map_node name f; (* node edits and associated executions *) @@ -122,31 +124,39 @@ fun nodes_of (Version nodes) = nodes; val node_of = get_node o nodes_of; -val node_names_of = Graph.keys o nodes_of; fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); +fun touch_descendants name nodes = + fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE))) + (Graph.all_succs nodes [name]) nodes; + fun edit_nodes (name, node_edit) (Version nodes) = Version - (case node_edit of - Clear => update_node name clear_node nodes - | Edits edits => update_node name (edit_node edits) nodes - | Header header => - let - val node = get_node nodes name; - val nodes' = Graph.new_node (name, node) (remove_node name nodes); - val parents = - (case header of Exn.Res (_, parents, _) => parents | _ => []) - |> filter (can (Graph.get_node nodes')); - val (header', nodes'') = - (header, Graph.add_deps_acyclic (name, parents) nodes') - handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes'); - in Graph.map_node name (set_header header') nodes'' end); + (touch_descendants name + (case node_edit of + Clear => update_node name clear_node nodes + | Edits edits => + nodes + |> update_node name (edit_node edits) + | Header header => + let + val node = get_node nodes name; + val nodes' = Graph.new_node (name, node) (remove_node name nodes); + val parents = + (case header of Exn.Res (_, parents, _) => parents | _ => []) + |> filter (can (Graph.get_node nodes')); + val (header', nodes'') = + (header, Graph.add_deps_acyclic (name, parents) nodes') + handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes') + | Graph.UNDEF d => (Exn.Exn (ERROR ("Undefined theory entry: " ^ quote d)), nodes') + in + nodes'' + |> Graph.map_node name (set_header header') + end)); -fun put_node name node (Version nodes) = - Version (nodes - |> Graph.default_node (name, empty_node) - |> Graph.map_node name (K node)); +fun def_node name (Version nodes) = Version (default_node name nodes); +fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes); end; @@ -157,7 +167,7 @@ abstype state = State of {versions: version Inttab.table, (*version_id -> document content*) commands: Toplevel.transition future Inttab.table, (*command_id -> transition (future parsing)*) - execs: (bool * Toplevel.state) lazy Inttab.table, (*exec_id -> execution process*) + execs: Toplevel.state lazy Inttab.table, (*exec_id -> execution process*) execution: unit future list} (*global execution process*) with @@ -170,7 +180,7 @@ val init_state = make_state (Inttab.make [(no_id, empty_version)], Inttab.make [(no_id, Future.value Toplevel.empty)], - Inttab.make [(no_id, Lazy.value (true, Toplevel.toplevel))], + Inttab.make [(no_id, empty_exec)], []); @@ -213,26 +223,17 @@ (* command executions *) -fun define_exec (id: exec_id) exec = +fun define_exec (exec_id, exec) = map_state (fn (versions, commands, execs, execution) => - let val execs' = Inttab.update_new (id, exec) execs + let val execs' = Inttab.update_new (exec_id, exec) execs handle Inttab.DUP dup => err_dup "command execution" dup in (versions, commands, execs', execution) end); -fun the_exec (State {execs, ...}) (id: exec_id) = - (case Inttab.lookup execs id of - NONE => err_undef "command execution" id +fun the_exec (State {execs, ...}) exec_id = + (case Inttab.lookup execs exec_id of + NONE => err_undef "command execution" exec_id | SOME exec => exec); -fun get_theory state version_id pos name = - let - val last = get_last (node_of (the_version state version_id) name); - val st = - (case Lazy.peek (the_exec state last) of - SOME result => #2 (Exn.release result) - | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos)); - in Toplevel.end_theory pos st end; - (* document execution *) @@ -275,20 +276,9 @@ in -fun run_command (node_name, node_header) raw_tr st = +fun run_command tr st = let - val is_init = Toplevel.is_init raw_tr; - val tr = - if is_init then - raw_tr |> Toplevel.modify_init (fn () => - let - (* FIXME get theories from document state *) - (* FIXME provide files via Scala layer *) - val (name, imports, uses) = Exn.release node_header; - val master = Path.dir (Path.explode node_name); - in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end) - else raw_tr; - + val is_init = Toplevel.is_init tr; val is_proof = Keyword.is_proof (Toplevel.name_of tr); val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof); @@ -300,12 +290,12 @@ val _ = List.app (Toplevel.error_msg tr) errs; in (case result of - NONE => (Toplevel.status tr Markup.failed; (false, st)) + NONE => (Toplevel.status tr Markup.failed; st) | SOME st' => (Toplevel.status tr Markup.finished; proof_status tr st'; if do_print then async_state tr st' else (); - (true, st'))) + st')) end; end; @@ -324,19 +314,16 @@ NONE => true | SOME exec' => exec' <> exec); -fun new_exec node_info (id: command_id) (exec_id, updates, state) = +fun new_exec (command_id, command) (assigns, execs, exec) = let - val exec = the_exec state exec_id; val exec_id' = new_id (); - val future_tr = the_command state id; val exec' = Lazy.lazy (fn () => let - val st = #2 (Lazy.force exec); - val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr); - in run_command node_info exec_tr st end); - val state' = define_exec exec_id' exec' state; - in (exec_id', (id, exec_id') :: updates, state') end; + val tr = Toplevel.put_id (print_id exec_id') (Future.get_finished command); + val st = Lazy.get_finished exec; + in run_command tr st end); + in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end; in @@ -344,34 +331,60 @@ let val old_version = the_version state old_id; val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 *) - val new_version = fold edit_nodes edits old_version; + val new_version = + old_version + |> fold (def_node o #1) edits + |> fold edit_nodes edits; + + val updates = + nodes_of new_version |> Graph.schedule + (fn deps => fn (name, node) => + (case first_entry NONE (is_changed (node_of old_version name)) node of + NONE => Future.value (([], [], []), node) + | SOME ((prev, id), _) => + let + fun init () = + let + val (thy_name, imports, uses) = Exn.release (get_header node); + (* FIXME provide files via Scala layer *) + val dir = Path.dir (Path.explode name); + val files = map (apfst Path.explode) uses; - fun update_node name (rev_updates, version, st) = - let - val node = node_of version name; - val header = get_header node; - in - (case first_entry NONE (is_changed (node_of old_version name)) node of - NONE => (rev_updates, version, st) - | SOME ((prev, id), _) => - let - val prev_exec = - (case prev of - NONE => no_id - | SOME prev_id => the_default no_id (the_entry node prev_id)); - val (last, rev_upds, st') = - fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st); - val node' = node |> fold update_entry rev_upds |> set_last last; - in (rev_upds @ rev_updates, put_node name node' version, st') end) - end; + val parents = + imports |> map (fn import => + (case AList.lookup (op =) deps import of + SOME parent_future => + get_theory (Position.file_only (import ^ ".thy")) + (#2 (Future.join parent_future)) + | NONE => Thy_Info.get_theory (Thy_Info.base_name import))); + in Thy_Load.begin_theory dir thy_name imports files parents end + fun get_command id = + (id, the_command state id |> Future.map (Toplevel.modify_init init)); + in + singleton + (Future.forks {name = "Document.edit", group = NONE, + deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}) + (fn () => + let + val prev_exec = + (case prev of + NONE => no_id + | SOME prev_id => the_default no_id (the_entry node prev_id)); + val (assigns, execs, result) = + fold_entries (SOME id) (new_exec o get_command o #2 o #1) + node ([], [], the_exec state prev_exec); + val node' = node + |> fold update_entry assigns + |> set_result result; + in ((assigns, execs, [(name, node')]), node') end) + end)) + |> Future.join_results |> Exn.release_all |> map #1; - (* FIXME Graph.schedule *) - val (rev_updates, new_version', state') = - fold update_node (node_names_of new_version) ([], new_version, state); - val state'' = define_version new_id new_version' state'; + val state' = state + |> fold (fold define_exec o #2) updates + |> define_version new_id (fold (fold put_node o #3) updates new_version); - val _ = join_commands state''; (* FIXME async!? *) - in (rev rev_updates, state'') end; + in (maps #1 (rev updates), state') end; end; @@ -386,13 +399,15 @@ fun force_exec NONE = () | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id)); - val execution' = (* FIXME Graph.schedule *) - Future.forks - {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true} - [fn () => - node_names_of version |> List.app (fn name => - fold_entries NONE (fn (_, exec) => fn () => force_exec exec) - (node_of version name) ())]; + val execution' = + nodes_of version |> Graph.schedule + (fn deps => fn (name, node) => + singleton + (Future.forks + {name = "theory:" ^ name, group = NONE, + deps = map (Future.task_of o #2) deps, + pri = 1, interrupts = true}) + (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node)); in (versions, commands, execs, execution') end);
--- a/src/Pure/PIDE/isar_document.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/PIDE/isar_document.ML Mon Aug 15 19:42:52 2011 -0700 @@ -33,6 +33,7 @@ val await_cancellation = Document.cancel_execution state; val (updates, state') = Document.edit old_id new_id edits state; val _ = await_cancellation (); + val _ = Document.join_commands state'; val _ = Output.status (Markup.markup (Markup.assign new_id) (implode (map (Markup.markup_only o Markup.edit) updates)));
--- a/src/Pure/Thy/thy_info.ML Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Pure/Thy/thy_info.ML Mon Aug 15 19:42:52 2011 -0700 @@ -9,6 +9,7 @@ sig datatype action = Update | Remove val add_hook: (action -> string -> unit) -> unit + val base_name: string -> string val get_names: unit -> string list val status: unit -> unit val lookup_theory: string -> theory option
--- a/src/Tools/jEdit/README.html Mon Aug 15 18:35:36 2011 -0700 +++ b/src/Tools/jEdit/README.html Mon Aug 15 19:42:52 2011 -0700 @@ -122,9 +122,8 @@ <li>No way to start/stop prover or switch to a different logic.<br/> <em>Workaround:</em> Change options and restart editor.</li> - <li>Multiple theory buffers cannot depend on each other, imports are - resolved via the file-system.<br/> - <em>Workaround:</em> Save/reload files manually.</li> + <li>Limited support for dependencies between multiple theory buffers.<br/> + <em>Workaround:</em> Load required files manually.</li> <li>No reclaiming of old/unused document versions in prover or editor.<br/>