merged
authorhuffman
Mon Aug 15 19:42:52 2011 -0700 (2011-08-15)
changeset 44220e5753e2a5944
parent 44219 f738e3200e24
parent 44204 3cdc4176638c
child 44221 bff7f7afb2db
merged
     1.1 --- a/src/HOL/Equiv_Relations.thy	Mon Aug 15 18:35:36 2011 -0700
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Aug 15 19:42:52 2011 -0700
     1.3 @@ -402,8 +402,8 @@
     1.4    by (erule part_equivpE, erule transpE)
     1.5  
     1.6  lemma part_equivp_typedef:
     1.7 -  "part_equivp R \<Longrightarrow> \<exists>d. d \<in> (\<lambda>c. \<exists>x. R x x \<and> c = R x)"
     1.8 -  by (auto elim: part_equivpE simp add: mem_def)
     1.9 +  "part_equivp R \<Longrightarrow> \<exists>d. d \<in> {c. \<exists>x. R x x \<and> c = Collect (R x)}"
    1.10 +  by (auto elim: part_equivpE)
    1.11  
    1.12  
    1.13  text {* Total equivalences *}
     2.1 --- a/src/HOL/Quotient.thy	Mon Aug 15 18:35:36 2011 -0700
     2.2 +++ b/src/HOL/Quotient.thy	Mon Aug 15 19:42:52 2011 -0700
     2.3 @@ -603,66 +603,52 @@
     2.4  
     2.5  locale quot_type =
     2.6    fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
     2.7 -  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
     2.8 -  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
     2.9 +  and   Abs :: "'a set \<Rightarrow> 'b"
    2.10 +  and   Rep :: "'b \<Rightarrow> 'a set"
    2.11    assumes equivp: "part_equivp R"
    2.12 -  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = R x"
    2.13 +  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = Collect (R x)"
    2.14    and     rep_inverse: "\<And>x. Abs (Rep x) = x"
    2.15 -  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = R x))) \<Longrightarrow> (Rep (Abs c)) = c"
    2.16 +  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = Collect (R x)))) \<Longrightarrow> (Rep (Abs c)) = c"
    2.17    and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
    2.18  begin
    2.19  
    2.20  definition
    2.21    abs :: "'a \<Rightarrow> 'b"
    2.22  where
    2.23 -  "abs x = Abs (R x)"
    2.24 +  "abs x = Abs (Collect (R x))"
    2.25  
    2.26  definition
    2.27    rep :: "'b \<Rightarrow> 'a"
    2.28  where
    2.29 -  "rep a = Eps (Rep a)"
    2.30 -
    2.31 -lemma homeier5:
    2.32 -  assumes a: "R r r"
    2.33 -  shows "Rep (Abs (R r)) = R r"
    2.34 -  apply (subst abs_inverse)
    2.35 -  using a by auto
    2.36 +  "rep a = (SOME x. x \<in> Rep a)"
    2.37  
    2.38 -theorem homeier6:
    2.39 -  assumes a: "R r r"
    2.40 -  and b: "R s s"
    2.41 -  shows "Abs (R r) = Abs (R s) \<longleftrightarrow> R r = R s"
    2.42 -  by (metis a b homeier5)
    2.43 -
    2.44 -theorem homeier8:
    2.45 +lemma some_collect:
    2.46    assumes "R r r"
    2.47 -  shows "R (Eps (R r)) = R r"
    2.48 -  using assms equivp[simplified part_equivp_def]
    2.49 -  apply clarify
    2.50 -  by (metis assms exE_some)
    2.51 +  shows "R (SOME x. x \<in> Collect (R r)) = R r"
    2.52 +  apply simp
    2.53 +  by (metis assms exE_some equivp[simplified part_equivp_def])
    2.54  
    2.55  lemma Quotient:
    2.56    shows "Quotient R abs rep"
    2.57    unfolding Quotient_def abs_def rep_def
    2.58    proof (intro conjI allI)
    2.59      fix a r s
    2.60 -    show "Abs (R (Eps (Rep a))) = a"
    2.61 -      using [[metis_new_skolemizer = false]]
    2.62 -      by (metis equivp exE_some part_equivp_def rep_inverse rep_prop)
    2.63 -    show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (R r) = Abs (R s))"
    2.64 -      by (metis homeier6 equivp[simplified part_equivp_def])
    2.65 -    show "R (Eps (Rep a)) (Eps (Rep a))" proof -
    2.66 -      obtain x where r: "R x x" and rep: "Rep a = R x" using rep_prop[of a] by auto
    2.67 -      have "R (Eps (R x)) x" using homeier8 r by simp
    2.68 -      then have "R x (Eps (R x))" using part_equivp_symp[OF equivp] by fast
    2.69 -      then have "R (Eps (R x)) (Eps (R x))" using homeier8[OF r] by simp
    2.70 -      then show "R (Eps (Rep a)) (Eps (Rep a))" using rep by simp
    2.71 +    show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
    2.72 +      obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto
    2.73 +      have "R (SOME x. x \<in> Rep a) x"  using r rep some_collect by metis
    2.74 +      then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
    2.75 +      then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
    2.76 +        using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`)
    2.77      qed
    2.78 -  qed
    2.79 -
    2.80 +    have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
    2.81 +    then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
    2.82 +    have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
    2.83 +      by (metis Collect_def abs_inverse)
    2.84 +    then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
    2.85 +      using equivp[simplified part_equivp_def] by metis
    2.86 +    qed
    2.87  end
    2.88  
    2.89 -
    2.90  subsection {* ML setup *}
    2.91  
    2.92  text {* Auxiliary data for the quotient package *}
     3.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Mon Aug 15 18:35:36 2011 -0700
     3.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Mon Aug 15 19:42:52 2011 -0700
     3.3 @@ -561,9 +561,9 @@
     3.4    shows "fset S = fset T \<longleftrightarrow> S = T"
     3.5    by (descending) (simp)
     3.6  
     3.7 -lemma filter_fset [simp]: 
     3.8 -  shows "fset (filter_fset P xs) = P \<inter> fset xs"
     3.9 -  by (descending) (auto simp add: mem_def)
    3.10 +lemma filter_fset [simp]:
    3.11 +  shows "fset (filter_fset P xs) = Collect P \<inter> fset xs"
    3.12 +  by (descending) (auto)
    3.13  
    3.14  lemma remove_fset [simp]: 
    3.15    shows "fset (remove_fset x xs) = fset xs - {x}"
     4.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Aug 15 18:35:36 2011 -0700
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Mon Aug 15 19:42:52 2011 -0700
     4.3 @@ -48,8 +48,8 @@
     4.4  
     4.5  (*** definition of quotient types ***)
     4.6  
     4.7 -val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)}
     4.8 -val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)}
     4.9 +val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
    4.10 +val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}
    4.11  
    4.12  (* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
    4.13  fun typedef_term rel rty lthy =
    4.14 @@ -58,9 +58,14 @@
    4.15        [("x", rty), ("c", HOLogic.mk_setT rty)]
    4.16        |> Variable.variant_frees lthy [rel]
    4.17        |> map Free
    4.18 +    fun mk_collect T =
    4.19 +      Const (@{const_name Collect}, (T --> @{typ bool}) --> HOLogic.mk_setT T)
    4.20 +    val collect_in = mk_collect rty
    4.21 +    val collect_out = mk_collect (HOLogic.mk_setT rty)
    4.22    in
    4.23 -    lambda c (HOLogic.exists_const rty $
    4.24 -        lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
    4.25 +    collect_out $ (lambda c (HOLogic.exists_const rty $
    4.26 +        lambda x (HOLogic.mk_conj (rel $ x $ x,
    4.27 +        HOLogic.mk_eq (c, collect_in $ (rel $ x))))))
    4.28    end
    4.29  
    4.30  
     5.1 --- a/src/Pure/Concurrent/future.ML	Mon Aug 15 18:35:36 2011 -0700
     5.2 +++ b/src/Pure/Concurrent/future.ML	Mon Aug 15 19:42:52 2011 -0700
     5.3 @@ -39,6 +39,7 @@
     5.4    val task_of: 'a future -> Task_Queue.task
     5.5    val peek: 'a future -> 'a Exn.result option
     5.6    val is_finished: 'a future -> bool
     5.7 +  val get_finished: 'a future -> 'a
     5.8    val interruptible_task: ('a -> 'b) -> 'a -> 'b
     5.9    val cancel_group: Task_Queue.group -> unit
    5.10    val cancel: 'a future -> unit
    5.11 @@ -105,6 +106,11 @@
    5.12  fun peek x = Single_Assignment.peek (result_of x);
    5.13  fun is_finished x = is_some (peek x);
    5.14  
    5.15 +fun get_finished x =
    5.16 +  (case peek x of
    5.17 +    SOME res => Exn.release res
    5.18 +  | NONE => raise Fail "Unfinished future evaluation");
    5.19 +
    5.20  
    5.21  
    5.22  (** scheduling **)
     6.1 --- a/src/Pure/Concurrent/lazy.ML	Mon Aug 15 18:35:36 2011 -0700
     6.2 +++ b/src/Pure/Concurrent/lazy.ML	Mon Aug 15 19:42:52 2011 -0700
     6.3 @@ -10,6 +10,8 @@
     6.4  sig
     6.5    type 'a lazy
     6.6    val peek: 'a lazy -> 'a Exn.result option
     6.7 +  val is_finished: 'a lazy -> bool
     6.8 +  val get_finished: 'a lazy -> 'a
     6.9    val lazy: (unit -> 'a) -> 'a lazy
    6.10    val value: 'a -> 'a lazy
    6.11    val force_result: 'a lazy -> 'a Exn.result
    6.12 @@ -36,6 +38,13 @@
    6.13  fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
    6.14  fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
    6.15  
    6.16 +fun is_finished x = is_some (peek x);
    6.17 +
    6.18 +fun get_finished x =
    6.19 +  (case peek x of
    6.20 +    SOME res => Exn.release res
    6.21 +  | NONE => raise Fail "Unfinished lazy evaluation");
    6.22 +
    6.23  
    6.24  (* force result *)
    6.25  
     7.1 --- a/src/Pure/Concurrent/lazy_sequential.ML	Mon Aug 15 18:35:36 2011 -0700
     7.2 +++ b/src/Pure/Concurrent/lazy_sequential.ML	Mon Aug 15 19:42:52 2011 -0700
     7.3 @@ -25,6 +25,13 @@
     7.4  fun lazy e = Lazy (Unsynchronized.ref (Expr e));
     7.5  fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a)));
     7.6  
     7.7 +fun is_finished x = is_some (peek x);
     7.8 +
     7.9 +fun get_finished x =
    7.10 +  (case peek x of
    7.11 +    SOME res => Exn.release res
    7.12 +  | NONE => raise Fail "Unfinished lazy evaluation");
    7.13 +
    7.14  
    7.15  (* force result *)
    7.16  
     8.1 --- a/src/Pure/General/graph.ML	Mon Aug 15 18:35:36 2011 -0700
     8.2 +++ b/src/Pure/General/graph.ML	Mon Aug 15 19:42:52 2011 -0700
     8.3 @@ -35,19 +35,19 @@
     8.4    val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
     8.5    val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
     8.6    val is_edge: 'a T -> key * key -> bool
     8.7 -  val add_edge: key * key -> 'a T -> 'a T
     8.8 -  val del_edge: key * key -> 'a T -> 'a T
     8.9 +  val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    8.10 +  val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    8.11    val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    8.12    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    8.13      'a T * 'a T -> 'a T                                               (*exception DUP*)
    8.14    val irreducible_paths: 'a T -> key * key -> key list list
    8.15    val all_paths: 'a T -> key * key -> key list list
    8.16    exception CYCLES of key list list
    8.17 -  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
    8.18 -  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
    8.19 +  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception UNDEF | CYCLES*)
    8.20 +  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception UNDEF | CYCLES*)
    8.21    val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
    8.22    val topological_order: 'a T -> key list
    8.23 -  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
    8.24 +  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception UNDEF | CYCLES*)
    8.25    val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    8.26    exception DEP of key * key
    8.27    val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
     9.1 --- a/src/Pure/General/position.ML	Mon Aug 15 18:35:36 2011 -0700
     9.2 +++ b/src/Pure/General/position.ML	Mon Aug 15 19:42:52 2011 -0700
     9.3 @@ -18,6 +18,7 @@
     9.4    val none: T
     9.5    val start: T
     9.6    val file_name: string -> Properties.T
     9.7 +  val file_only: string -> T
     9.8    val file: string -> T
     9.9    val line: int -> T
    9.10    val line_file: int -> string -> T
    9.11 @@ -104,6 +105,7 @@
    9.12  fun file_name "" = []
    9.13    | file_name name = [(Markup.fileN, name)];
    9.14  
    9.15 +fun file_only name = Pos ((0, 0, 0), file_name name);
    9.16  fun file name = Pos ((1, 1, 0), file_name name);
    9.17  
    9.18  fun line_file i name = Pos ((i, 1, 0), file_name name);
    10.1 --- a/src/Pure/General/secure.ML	Mon Aug 15 18:35:36 2011 -0700
    10.2 +++ b/src/Pure/General/secure.ML	Mon Aug 15 19:42:52 2011 -0700
    10.3 @@ -63,7 +63,7 @@
    10.4  val use_file = Secure.use_file;
    10.5  
    10.6  fun use s =
    10.7 -  Position.setmp_thread_data (Position.of_properties (Position.file_name s))
    10.8 +  Position.setmp_thread_data (Position.file_only s)
    10.9      (fn () =>
   10.10        Secure.use_file ML_Parse.global_context true s
   10.11          handle ERROR msg => (writeln msg; error "ML error")) ();
    11.1 --- a/src/Pure/Isar/toplevel.ML	Mon Aug 15 18:35:36 2011 -0700
    11.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Aug 15 19:42:52 2011 -0700
    11.3 @@ -185,8 +185,8 @@
    11.4    | _ => raise UNDEF);
    11.5  
    11.6  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
    11.7 -  | end_theory pos (State (NONE, _)) = error ("Missing theory " ^ Position.str_of pos)
    11.8 -  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory " ^ Position.str_of pos);
    11.9 +  | end_theory pos (State (NONE, _)) = error ("Missing theory" ^ Position.str_of pos)
   11.10 +  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
   11.11  
   11.12  
   11.13  (* print state *)
    12.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 15 18:35:36 2011 -0700
    12.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 15 19:42:52 2011 -0700
    12.3 @@ -23,7 +23,7 @@
    12.4    type edit = string * node_edit
    12.5    type state
    12.6    val init_state: state
    12.7 -  val get_theory: state -> version_id -> Position.T -> string -> theory
    12.8 +  val join_commands: state -> unit
    12.9    val cancel_execution: state -> unit -> unit
   12.10    val define_command: command_id -> string -> state -> state
   12.11    val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
   12.12 @@ -61,32 +61,34 @@
   12.13  abstype node = Node of
   12.14   {header: node_header,
   12.15    entries: exec_id option Entries.T,  (*command entries with excecutions*)
   12.16 -  last: exec_id}  (*last entry with main result*)
   12.17 +  result: Toplevel.state lazy}
   12.18  and version = Version of node Graph.T  (*development graph wrt. static imports*)
   12.19  with
   12.20  
   12.21 -fun make_node (header, entries, last) =
   12.22 -  Node {header = header, entries = entries, last = last};
   12.23 +fun make_node (header, entries, result) =
   12.24 +  Node {header = header, entries = entries, result = result};
   12.25  
   12.26 -fun map_node f (Node {header, entries, last}) =
   12.27 -  make_node (f (header, entries, last));
   12.28 +fun map_node f (Node {header, entries, result}) =
   12.29 +  make_node (f (header, entries, result));
   12.30  
   12.31  fun get_header (Node {header, ...}) = header;
   12.32 -fun set_header header = map_node (fn (_, entries, last) => (header, entries, last));
   12.33 +fun set_header header = map_node (fn (_, entries, result) => (header, entries, result));
   12.34  
   12.35 -fun map_entries f (Node {header, entries, last}) = make_node (header, f entries, last);
   12.36 +fun map_entries f (Node {header, entries, result}) = make_node (header, f entries, result);
   12.37  fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
   12.38  fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
   12.39  
   12.40 -fun get_last (Node {last, ...}) = last;
   12.41 -fun set_last last = map_node (fn (header, entries, _) => (header, entries, last));
   12.42 +fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result);
   12.43 +fun set_result result = map_node (fn (header, entries, _) => (header, entries, result));
   12.44  
   12.45 -val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id);
   12.46 -val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id));
   12.47 +val empty_exec = Lazy.value Toplevel.toplevel;
   12.48 +val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, empty_exec);
   12.49 +val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, empty_exec));
   12.50  
   12.51  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
   12.52  fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
   12.53 -fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f;
   12.54 +fun default_node name = Graph.default_node (name, empty_node);
   12.55 +fun update_node name f = default_node name #> Graph.map_node name f;
   12.56  
   12.57  
   12.58  (* node edits and associated executions *)
   12.59 @@ -122,31 +124,39 @@
   12.60  
   12.61  fun nodes_of (Version nodes) = nodes;
   12.62  val node_of = get_node o nodes_of;
   12.63 -val node_names_of = Graph.keys o nodes_of;
   12.64  
   12.65  fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
   12.66  
   12.67 +fun touch_descendants name nodes =
   12.68 +  fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE)))
   12.69 +    (Graph.all_succs nodes [name]) nodes;
   12.70 +
   12.71  fun edit_nodes (name, node_edit) (Version nodes) =
   12.72    Version
   12.73 -    (case node_edit of
   12.74 -      Clear => update_node name clear_node nodes
   12.75 -    | Edits edits => update_node name (edit_node edits) nodes
   12.76 -    | Header header =>
   12.77 -        let
   12.78 -          val node = get_node nodes name;
   12.79 -          val nodes' = Graph.new_node (name, node) (remove_node name nodes);
   12.80 -          val parents =
   12.81 -            (case header of Exn.Res (_, parents, _) => parents | _ => [])
   12.82 -            |> filter (can (Graph.get_node nodes'));
   12.83 -          val (header', nodes'') =
   12.84 -            (header, Graph.add_deps_acyclic (name, parents) nodes')
   12.85 -              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes');
   12.86 -        in Graph.map_node name (set_header header') nodes'' end);
   12.87 +    (touch_descendants name
   12.88 +      (case node_edit of
   12.89 +        Clear => update_node name clear_node nodes
   12.90 +      | Edits edits =>
   12.91 +          nodes
   12.92 +          |> update_node name (edit_node edits)
   12.93 +      | Header header =>
   12.94 +          let
   12.95 +            val node = get_node nodes name;
   12.96 +            val nodes' = Graph.new_node (name, node) (remove_node name nodes);
   12.97 +            val parents =
   12.98 +              (case header of Exn.Res (_, parents, _) => parents | _ => [])
   12.99 +              |> filter (can (Graph.get_node nodes'));
  12.100 +            val (header', nodes'') =
  12.101 +              (header, Graph.add_deps_acyclic (name, parents) nodes')
  12.102 +                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes')
  12.103 +                  | Graph.UNDEF d => (Exn.Exn (ERROR ("Undefined theory entry: " ^ quote d)), nodes')
  12.104 +          in
  12.105 +            nodes''
  12.106 +            |> Graph.map_node name (set_header header')
  12.107 +          end));
  12.108  
  12.109 -fun put_node name node (Version nodes) =
  12.110 -  Version (nodes
  12.111 -    |> Graph.default_node (name, empty_node)
  12.112 -    |> Graph.map_node name (K node));
  12.113 +fun def_node name (Version nodes) = Version (default_node name nodes);
  12.114 +fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes);
  12.115  
  12.116  end;
  12.117  
  12.118 @@ -157,7 +167,7 @@
  12.119  abstype state = State of
  12.120   {versions: version Inttab.table,  (*version_id -> document content*)
  12.121    commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
  12.122 -  execs: (bool * Toplevel.state) lazy Inttab.table,  (*exec_id -> execution process*)
  12.123 +  execs: Toplevel.state lazy Inttab.table,  (*exec_id -> execution process*)
  12.124    execution: unit future list}  (*global execution process*)
  12.125  with
  12.126  
  12.127 @@ -170,7 +180,7 @@
  12.128  val init_state =
  12.129    make_state (Inttab.make [(no_id, empty_version)],
  12.130      Inttab.make [(no_id, Future.value Toplevel.empty)],
  12.131 -    Inttab.make [(no_id, Lazy.value (true, Toplevel.toplevel))],
  12.132 +    Inttab.make [(no_id, empty_exec)],
  12.133      []);
  12.134  
  12.135  
  12.136 @@ -213,26 +223,17 @@
  12.137  
  12.138  (* command executions *)
  12.139  
  12.140 -fun define_exec (id: exec_id) exec =
  12.141 +fun define_exec (exec_id, exec) =
  12.142    map_state (fn (versions, commands, execs, execution) =>
  12.143 -    let val execs' = Inttab.update_new (id, exec) execs
  12.144 +    let val execs' = Inttab.update_new (exec_id, exec) execs
  12.145        handle Inttab.DUP dup => err_dup "command execution" dup
  12.146      in (versions, commands, execs', execution) end);
  12.147  
  12.148 -fun the_exec (State {execs, ...}) (id: exec_id) =
  12.149 -  (case Inttab.lookup execs id of
  12.150 -    NONE => err_undef "command execution" id
  12.151 +fun the_exec (State {execs, ...}) exec_id =
  12.152 +  (case Inttab.lookup execs exec_id of
  12.153 +    NONE => err_undef "command execution" exec_id
  12.154    | SOME exec => exec);
  12.155  
  12.156 -fun get_theory state version_id pos name =
  12.157 -  let
  12.158 -    val last = get_last (node_of (the_version state version_id) name);
  12.159 -    val st =
  12.160 -      (case Lazy.peek (the_exec state last) of
  12.161 -        SOME result => #2 (Exn.release result)
  12.162 -      | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos));
  12.163 -  in Toplevel.end_theory pos st end;
  12.164 -
  12.165  
  12.166  (* document execution *)
  12.167  
  12.168 @@ -275,20 +276,9 @@
  12.169  
  12.170  in
  12.171  
  12.172 -fun run_command (node_name, node_header) raw_tr st =
  12.173 +fun run_command tr st =
  12.174    let
  12.175 -    val is_init = Toplevel.is_init raw_tr;
  12.176 -    val tr =
  12.177 -      if is_init then
  12.178 -        raw_tr |> Toplevel.modify_init (fn () =>
  12.179 -          let
  12.180 -            (* FIXME get theories from document state *)
  12.181 -            (* FIXME provide files via Scala layer *)
  12.182 -            val (name, imports, uses) = Exn.release node_header;
  12.183 -            val master = Path.dir (Path.explode node_name);
  12.184 -          in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end)
  12.185 -      else raw_tr;
  12.186 -
  12.187 +    val is_init = Toplevel.is_init tr;
  12.188      val is_proof = Keyword.is_proof (Toplevel.name_of tr);
  12.189      val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
  12.190  
  12.191 @@ -300,12 +290,12 @@
  12.192      val _ = List.app (Toplevel.error_msg tr) errs;
  12.193    in
  12.194      (case result of
  12.195 -      NONE => (Toplevel.status tr Markup.failed; (false, st))
  12.196 +      NONE => (Toplevel.status tr Markup.failed; st)
  12.197      | SOME st' =>
  12.198         (Toplevel.status tr Markup.finished;
  12.199          proof_status tr st';
  12.200          if do_print then async_state tr st' else ();
  12.201 -        (true, st')))
  12.202 +        st'))
  12.203    end;
  12.204  
  12.205  end;
  12.206 @@ -324,19 +314,16 @@
  12.207      NONE => true
  12.208    | SOME exec' => exec' <> exec);
  12.209  
  12.210 -fun new_exec node_info (id: command_id) (exec_id, updates, state) =
  12.211 +fun new_exec (command_id, command) (assigns, execs, exec) =
  12.212    let
  12.213 -    val exec = the_exec state exec_id;
  12.214      val exec_id' = new_id ();
  12.215 -    val future_tr = the_command state id;
  12.216      val exec' =
  12.217        Lazy.lazy (fn () =>
  12.218          let
  12.219 -          val st = #2 (Lazy.force exec);
  12.220 -          val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
  12.221 -        in run_command node_info exec_tr st end);
  12.222 -    val state' = define_exec exec_id' exec' state;
  12.223 -  in (exec_id', (id, exec_id') :: updates, state') end;
  12.224 +          val tr = Toplevel.put_id (print_id exec_id') (Future.get_finished command);
  12.225 +          val st = Lazy.get_finished exec;
  12.226 +        in run_command tr st end);
  12.227 +  in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end;
  12.228  
  12.229  in
  12.230  
  12.231 @@ -344,34 +331,60 @@
  12.232    let
  12.233      val old_version = the_version state old_id;
  12.234      val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
  12.235 -    val new_version = fold edit_nodes edits old_version;
  12.236 +    val new_version =
  12.237 +      old_version
  12.238 +      |> fold (def_node o #1) edits
  12.239 +      |> fold edit_nodes edits;
  12.240 +
  12.241 +    val updates =
  12.242 +      nodes_of new_version |> Graph.schedule
  12.243 +        (fn deps => fn (name, node) =>
  12.244 +          (case first_entry NONE (is_changed (node_of old_version name)) node of
  12.245 +            NONE => Future.value (([], [], []), node)
  12.246 +          | SOME ((prev, id), _) =>
  12.247 +              let
  12.248 +                fun init () =
  12.249 +                  let
  12.250 +                    val (thy_name, imports, uses) = Exn.release (get_header node);
  12.251 +                    (* FIXME provide files via Scala layer *)
  12.252 +                    val dir = Path.dir (Path.explode name);
  12.253 +                    val files = map (apfst Path.explode) uses;
  12.254  
  12.255 -    fun update_node name (rev_updates, version, st) =
  12.256 -      let
  12.257 -        val node = node_of version name;
  12.258 -        val header = get_header node;
  12.259 -      in
  12.260 -        (case first_entry NONE (is_changed (node_of old_version name)) node of
  12.261 -          NONE => (rev_updates, version, st)
  12.262 -        | SOME ((prev, id), _) =>
  12.263 -            let
  12.264 -              val prev_exec =
  12.265 -                (case prev of
  12.266 -                  NONE => no_id
  12.267 -                | SOME prev_id => the_default no_id (the_entry node prev_id));
  12.268 -              val (last, rev_upds, st') =
  12.269 -                fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st);
  12.270 -              val node' = node |> fold update_entry rev_upds |> set_last last;
  12.271 -            in (rev_upds @ rev_updates, put_node name node' version, st') end)
  12.272 -      end;
  12.273 +                    val parents =
  12.274 +                      imports |> map (fn import =>
  12.275 +                        (case AList.lookup (op =) deps import of
  12.276 +                          SOME parent_future =>
  12.277 +                            get_theory (Position.file_only (import ^ ".thy"))
  12.278 +                              (#2 (Future.join parent_future))
  12.279 +                        | NONE => Thy_Info.get_theory (Thy_Info.base_name import)));
  12.280 +                  in Thy_Load.begin_theory dir thy_name imports files parents end
  12.281 +                fun get_command id =
  12.282 +                  (id, the_command state id |> Future.map (Toplevel.modify_init init));
  12.283 +              in
  12.284 +                singleton
  12.285 +                  (Future.forks {name = "Document.edit", group = NONE,
  12.286 +                    deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false})
  12.287 +                  (fn () =>
  12.288 +                    let
  12.289 +                      val prev_exec =
  12.290 +                        (case prev of
  12.291 +                          NONE => no_id
  12.292 +                        | SOME prev_id => the_default no_id (the_entry node prev_id));
  12.293 +                      val (assigns, execs, result) =
  12.294 +                        fold_entries (SOME id) (new_exec o get_command o #2 o #1)
  12.295 +                          node ([], [], the_exec state prev_exec);
  12.296 +                      val node' = node
  12.297 +                        |> fold update_entry assigns
  12.298 +                        |> set_result result;
  12.299 +                    in ((assigns, execs, [(name, node')]), node') end)
  12.300 +              end))
  12.301 +      |> Future.join_results |> Exn.release_all |> map #1;
  12.302  
  12.303 -    (* FIXME Graph.schedule *)
  12.304 -    val (rev_updates, new_version', state') =
  12.305 -      fold update_node (node_names_of new_version) ([], new_version, state);
  12.306 -    val state'' = define_version new_id new_version' state';
  12.307 +    val state' = state
  12.308 +      |> fold (fold define_exec o #2) updates
  12.309 +      |> define_version new_id (fold (fold put_node o #3) updates new_version);
  12.310  
  12.311 -    val _ = join_commands state'';  (* FIXME async!? *)
  12.312 -  in (rev rev_updates, state'') end;
  12.313 +  in (maps #1 (rev updates), state') end;
  12.314  
  12.315  end;
  12.316  
  12.317 @@ -386,13 +399,15 @@
  12.318        fun force_exec NONE = ()
  12.319          | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
  12.320  
  12.321 -      val execution' = (* FIXME Graph.schedule *)
  12.322 -        Future.forks
  12.323 -          {name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true}
  12.324 -          [fn () =>
  12.325 -            node_names_of version |> List.app (fn name =>
  12.326 -              fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
  12.327 -                  (node_of version name) ())];
  12.328 +      val execution' =
  12.329 +        nodes_of version |> Graph.schedule
  12.330 +          (fn deps => fn (name, node) =>
  12.331 +            singleton
  12.332 +              (Future.forks
  12.333 +                {name = "theory:" ^ name, group = NONE,
  12.334 +                  deps = map (Future.task_of o #2) deps,
  12.335 +                  pri = 1, interrupts = true})
  12.336 +              (fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node));
  12.337  
  12.338      in (versions, commands, execs, execution') end);
  12.339  
    13.1 --- a/src/Pure/PIDE/isar_document.ML	Mon Aug 15 18:35:36 2011 -0700
    13.2 +++ b/src/Pure/PIDE/isar_document.ML	Mon Aug 15 19:42:52 2011 -0700
    13.3 @@ -33,6 +33,7 @@
    13.4        val await_cancellation = Document.cancel_execution state;
    13.5        val (updates, state') = Document.edit old_id new_id edits state;
    13.6        val _ = await_cancellation ();
    13.7 +      val _ = Document.join_commands state';
    13.8        val _ =
    13.9          Output.status (Markup.markup (Markup.assign new_id)
   13.10            (implode (map (Markup.markup_only o Markup.edit) updates)));
    14.1 --- a/src/Pure/Thy/thy_info.ML	Mon Aug 15 18:35:36 2011 -0700
    14.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Aug 15 19:42:52 2011 -0700
    14.3 @@ -9,6 +9,7 @@
    14.4  sig
    14.5    datatype action = Update | Remove
    14.6    val add_hook: (action -> string -> unit) -> unit
    14.7 +  val base_name: string -> string
    14.8    val get_names: unit -> string list
    14.9    val status: unit -> unit
   14.10    val lookup_theory: string -> theory option
    15.1 --- a/src/Tools/jEdit/README.html	Mon Aug 15 18:35:36 2011 -0700
    15.2 +++ b/src/Tools/jEdit/README.html	Mon Aug 15 19:42:52 2011 -0700
    15.3 @@ -122,9 +122,8 @@
    15.4    <li>No way to start/stop prover or switch to a different logic.<br/>
    15.5    <em>Workaround:</em> Change options and restart editor.</li>
    15.6  
    15.7 -  <li>Multiple theory buffers cannot depend on each other, imports are
    15.8 -  resolved via the file-system.<br/>
    15.9 -  <em>Workaround:</em> Save/reload files manually.</li>
   15.10 +  <li>Limited support for dependencies between multiple theory buffers.<br/>
   15.11 +  <em>Workaround:</em> Load required files manually.</li>
   15.12  
   15.13    <li>No reclaiming of old/unused document versions in prover or
   15.14    editor.<br/>