--- a/src/HOL/Algebra/Congruence.thy Fri Aug 26 15:11:26 2011 -0700
+++ b/src/HOL/Algebra/Congruence.thy Fri Aug 26 15:11:33 2011 -0700
@@ -29,15 +29,15 @@
where "A {.=}\<^bsub>S\<^esub> B \<longleftrightarrow> ((\<forall>x \<in> A. x .\<in>\<^bsub>S\<^esub> B) \<and> (\<forall>x \<in> B. x .\<in>\<^bsub>S\<^esub> A))"
definition
- eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index> _")
+ eq_class_of :: "_ \<Rightarrow> 'a \<Rightarrow> 'a set" ("class'_of\<index>")
where "class_of\<^bsub>S\<^esub> x = {y \<in> carrier S. x .=\<^bsub>S\<^esub> y}"
definition
- eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index> _")
+ eq_closure_of :: "_ \<Rightarrow> 'a set \<Rightarrow> 'a set" ("closure'_of\<index>")
where "closure_of\<^bsub>S\<^esub> A = {y \<in> carrier S. y .\<in>\<^bsub>S\<^esub> A}"
definition
- eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index> _")
+ eq_is_closed :: "_ \<Rightarrow> 'a set \<Rightarrow> bool" ("is'_closed\<index>")
where "is_closed\<^bsub>S\<^esub> A \<longleftrightarrow> A \<subseteq> carrier S \<and> closure_of\<^bsub>S\<^esub> A = A"
abbreviation
--- a/src/HOL/Algebra/Group.thy Fri Aug 26 15:11:26 2011 -0700
+++ b/src/HOL/Algebra/Group.thy Fri Aug 26 15:11:33 2011 -0700
@@ -154,7 +154,7 @@
and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
then have "(inv x \<otimes> x) \<otimes> y = (inv x \<otimes> x) \<otimes> z"
by (simp add: m_assoc Units_closed del: Units_l_inv)
- with G show "y = z" by (simp add: Units_l_inv)
+ with G show "y = z" by simp
next
assume eq: "y = z"
and G: "x \<in> Units G" "y \<in> carrier G" "z \<in> carrier G"
@@ -332,7 +332,7 @@
proof -
assume x: "x \<in> carrier G"
then have "inv x \<otimes> (x \<otimes> inv x) = inv x \<otimes> \<one>"
- by (simp add: m_assoc [symmetric] l_inv)
+ by (simp add: m_assoc [symmetric])
with x show ?thesis by (simp del: r_one)
qed
@@ -372,7 +372,7 @@
proof -
assume G: "x \<in> carrier G" "y \<in> carrier G"
then have "inv (x \<otimes> y) \<otimes> (x \<otimes> y) = (inv y \<otimes> inv x) \<otimes> (x \<otimes> y)"
- by (simp add: m_assoc l_inv) (simp add: m_assoc [symmetric])
+ by (simp add: m_assoc) (simp add: m_assoc [symmetric])
with G show ?thesis by (simp del: l_inv Units_l_inv)
qed
@@ -446,7 +446,7 @@
lemma (in group) one_in_subset:
"[| H \<subseteq> carrier G; H \<noteq> {}; \<forall>a \<in> H. inv a \<in> H; \<forall>a\<in>H. \<forall>b\<in>H. a \<otimes> b \<in> H |]
==> \<one> \<in> H"
-by (force simp add: l_inv)
+by force
text {* A characterization of subgroups: closed, non-empty subset. *}
--- a/src/HOL/Algebra/Lattice.thy Fri Aug 26 15:11:26 2011 -0700
+++ b/src/HOL/Algebra/Lattice.thy Fri Aug 26 15:11:33 2011 -0700
@@ -34,7 +34,8 @@
subsubsection {* The order relation *}
-context weak_partial_order begin
+context weak_partial_order
+begin
lemma le_cong_l [intro, trans]:
"\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
@@ -85,7 +86,7 @@
and yy': "y .= y'"
and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
shows "x \<sqsubset> y'"
- using assms unfolding lless_def by (auto intro: trans sym)
+ using assms unfolding lless_def by (auto intro: trans sym) (*slow*)
lemma (in weak_partial_order) lless_antisym:
@@ -574,8 +575,7 @@
proof (cases "A = {}")
case True
with insert show ?thesis
- by simp (simp add: least_cong [OF weak_sup_of_singleton]
- sup_of_singleton_closed sup_of_singletonI)
+ by simp (simp add: least_cong [OF weak_sup_of_singleton] sup_of_singletonI)
(* The above step is hairy; least_cong can make simp loop.
Would want special version of simp to apply least_cong. *)
next
@@ -1282,7 +1282,7 @@
(is "complete_lattice ?L")
proof (rule partial_order.complete_latticeI)
show "partial_order ?L"
- proof qed auto
+ by default auto
next
fix B
assume B: "B \<subseteq> carrier ?L"
--- a/src/Pure/General/linear_set.ML Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/General/linear_set.ML Fri Aug 26 15:11:33 2011 -0700
@@ -14,12 +14,10 @@
val empty: 'a T
val is_empty: 'a T -> bool
val defined: 'a T -> key -> bool
- val lookup: 'a T -> key -> 'a option
+ val lookup: 'a T -> key -> ('a * key option) option
val update: key * 'a -> 'a T -> 'a T
- val fold: key option ->
- ((key option * key) * 'a -> 'b -> 'b) -> 'a T -> 'b -> 'b
- val get_first: key option ->
- ((key option * key) * 'a -> bool) -> 'a T -> ((key option * key) * 'a) option
+ val iterate: key option ->
+ ((key option * key) * 'a -> 'b -> 'b option) -> 'a T -> 'b -> 'b
val get_after: 'a T -> key option -> key option
val insert_after: key option -> key * 'a -> 'a T -> 'a T
val delete_after: key option -> 'a T -> 'a T
@@ -70,7 +68,7 @@
fun defined set key = Table.defined (entries_of set) key;
-fun lookup set key = Option.map fst (Table.lookup (entries_of set) key);
+fun lookup set key = Table.lookup (entries_of set) key;
fun update (key, x) = map_set (fn (start, entries) =>
(start, put_entry (key, (x, next_entry entries key)) entries));
@@ -81,7 +79,7 @@
fun optional_start set NONE = start_of set
| optional_start _ some = some;
-fun fold opt_start f set =
+fun iterate opt_start f set =
let
val entries = entries_of set;
fun apply _ NONE y = y
@@ -89,20 +87,13 @@
let
val (x, next) = the_entry entries key;
val item = ((prev, key), x);
- in apply (SOME key) next (f item y) end;
+ in
+ (case f item y of
+ NONE => y
+ | SOME y' => apply (SOME key) next y')
+ end;
in apply NONE (optional_start set opt_start) end;
-fun get_first opt_start P set =
- let
- val entries = entries_of set;
- fun first _ NONE = NONE
- | first prev (SOME key) =
- let
- val (x, next) = the_entry entries key;
- val item = ((prev, key), x);
- in if P item then SOME item else first (SOME key) next end;
- in first NONE (optional_start set opt_start) end;
-
(* relative addressing *)
--- a/src/Pure/General/markup.ML Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/General/markup.ML Fri Aug 26 15:11:33 2011 -0700
@@ -108,9 +108,7 @@
val failedN: string val failed: T
val finishedN: string val finished: T
val versionN: string
- val execN: string
val assignN: string val assign: int -> T
- val editN: string val edit: int * int -> T
val serialN: string
val promptN: string val prompt: T
val readyN: string val ready: T
@@ -353,12 +351,8 @@
(* interactive documents *)
val versionN = "version";
-val execN = "exec";
val (assignN, assign) = markup_int "assign" versionN;
-val editN = "edit";
-fun edit (cmd_id, exec_id) : T = (editN, [(idN, print_int cmd_id), (execN, print_int exec_id)]);
-
(* messages *)
--- a/src/Pure/General/markup.scala Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/General/markup.scala Fri Aug 26 15:11:33 2011 -0700
@@ -232,9 +232,7 @@
/* interactive documents */
val VERSION = "version"
- val EXEC = "exec"
val ASSIGN = "assign"
- val EDIT = "edit"
/* prover process */
--- a/src/Pure/Isar/outer_syntax.ML Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/Isar/outer_syntax.ML Fri Aug 26 15:11:33 2011 -0700
@@ -34,10 +34,10 @@
val process_file: Path.T -> theory -> theory
type isar
val isar: TextIO.instream -> bool -> isar
- val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
- val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
+ val read_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
+ val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
(Toplevel.transition * Toplevel.transition list) list
- val prepare_command: Position.T -> string -> Toplevel.transition
+ val read_command: Position.T -> string -> Toplevel.transition
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -251,11 +251,11 @@
|> toplevel_source term (SOME true) lookup_commands_dynamic;
-(* prepare toplevel commands -- fail-safe *)
+(* read toplevel commands -- fail-safe *)
val not_singleton = "Exactly one command expected";
-fun prepare_span outer_syntax span =
+fun read_span outer_syntax span =
let
val commands = lookup_commands outer_syntax;
val range_pos = Position.set_range (Thy_Syntax.span_range span);
@@ -272,19 +272,19 @@
handle ERROR msg => (Toplevel.malformed range_pos msg, true)
end;
-fun prepare_element outer_syntax init {head, proof, proper_proof} =
+fun read_element outer_syntax init {head, proof, proper_proof} =
let
- val (tr, proper_head) = prepare_span outer_syntax head |>> Toplevel.modify_init init;
- val proof_trs = map (prepare_span outer_syntax) proof |> filter #2 |> map #1;
+ val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
+ val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
in
if proper_head andalso proper_proof then [(tr, proof_trs)]
else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
end;
-fun prepare_command pos str =
+fun read_command pos str =
let val (lexs, outer_syntax) = get_syntax () in
(case Thy_Syntax.parse_spans lexs pos str of
- [span] => #1 (prepare_span outer_syntax span)
+ [span] => #1 (read_span outer_syntax span)
| _ => Toplevel.malformed pos not_singleton)
end;
--- a/src/Pure/PIDE/command.scala Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/PIDE/command.scala Fri Aug 26 15:11:33 2011 -0700
@@ -88,14 +88,22 @@
/* perspective */
- type Perspective = List[Command] // visible commands in canonical order
+ object Perspective
+ {
+ val empty: Perspective = Perspective(Nil)
+ }
- def equal_perspective(p1: Perspective, p2: Perspective): Boolean =
+ sealed case class Perspective(commands: List[Command]) // visible commands in canonical order
{
- require(p1.forall(_.is_defined))
- require(p2.forall(_.is_defined))
- p1.length == p2.length &&
- (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
+ def same(that: Perspective): Boolean =
+ {
+ val cmds1 = this.commands
+ val cmds2 = that.commands
+ require(cmds1.forall(_.is_defined))
+ require(cmds2.forall(_.is_defined))
+ cmds1.length == cmds2.length &&
+ (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
+ }
}
}
--- a/src/Pure/PIDE/document.ML Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/PIDE/document.ML Fri Aug 26 15:11:33 2011 -0700
@@ -2,7 +2,7 @@
Author: Makarius
Document as collection of named nodes, each consisting of an editable
-list of commands, associated with asynchronous execution process.
+list of commands, with asynchronous read/eval/print processes.
*)
signature DOCUMENT =
@@ -28,7 +28,8 @@
val join_commands: state -> unit
val cancel_execution: state -> Future.task list
val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
- val edit: version_id -> version_id -> edit list -> state -> (command_id * exec_id) list * state
+ val update: version_id -> version_id -> edit list -> state ->
+ ((command_id * exec_id option) list * (string * command_id option) list) * state
val execute: version_id -> state -> state
val state: unit -> state
val change_state: (state -> state) -> unit
@@ -58,7 +59,7 @@
(** document structure **)
type node_header = (string * string list * (string * bool) list) Exn.result;
-type perspective = (command_id -> bool) * command_id list; (*visible commands, canonical order*)
+type perspective = (command_id -> bool) * command_id option; (*visible commands, last*)
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
abstype node = Node of
@@ -66,58 +67,62 @@
header: node_header,
perspective: perspective,
entries: exec_id option Entries.T, (*command entries with excecutions*)
+ last_exec: command_id option, (*last command with exec state assignment*)
result: Toplevel.state lazy}
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-fun make_node (touched, header, perspective, entries, result) =
+fun make_node (touched, header, perspective, entries, last_exec, result) =
Node {touched = touched, header = header, perspective = perspective,
- entries = entries, result = result};
+ entries = entries, last_exec = last_exec, result = result};
-fun map_node f (Node {touched, header, perspective, entries, result}) =
- make_node (f (touched, header, perspective, entries, result));
+fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) =
+ make_node (f (touched, header, perspective, entries, last_exec, result));
-fun make_perspective ids : perspective =
- (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids);
+fun make_perspective command_ids : perspective =
+ (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
+val no_header = Exn.Exn (ERROR "Bad theory header");
val no_perspective = make_perspective [];
val no_print = Lazy.value ();
val no_result = Lazy.value Toplevel.toplevel;
-val empty_node =
- make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
-
-val clear_node =
- map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, no_result));
+val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result);
+val clear_node = map_node (fn (_, header, _, _, _, _) =>
+ (false, header, no_perspective, Entries.empty, NONE, no_result));
(* basic components *)
fun is_touched (Node {touched, ...}) = touched;
fun set_touched touched =
- map_node (fn (_, header, perspective, entries, result) =>
- (touched, header, perspective, entries, result));
+ map_node (fn (_, header, perspective, entries, last_exec, result) =>
+ (touched, header, perspective, entries, last_exec, result));
fun get_header (Node {header, ...}) = header;
fun set_header header =
- map_node (fn (touched, _, perspective, entries, result) =>
- (touched, header, perspective, entries, result));
+ map_node (fn (touched, _, perspective, entries, last_exec, result) =>
+ (touched, header, perspective, entries, last_exec, result));
fun get_perspective (Node {perspective, ...}) = perspective;
fun set_perspective ids =
- map_node (fn (touched, header, _, entries, result) =>
- (touched, header, make_perspective ids, entries, result));
+ map_node (fn (touched, header, _, entries, last_exec, result) =>
+ (touched, header, make_perspective ids, entries, last_exec, result));
fun map_entries f =
- map_node (fn (touched, header, perspective, entries, result) =>
- (touched, header, perspective, 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;
+ map_node (fn (touched, header, perspective, entries, last_exec, result) =>
+ (touched, header, perspective, f entries, last_exec, result));
+fun iterate_entries start f (Node {entries, ...}) = Entries.iterate start f entries;
+
+fun get_last_exec (Node {last_exec, ...}) = last_exec;
+fun set_last_exec last_exec =
+ map_node (fn (touched, header, perspective, entries, _, result) =>
+ (touched, header, perspective, entries, last_exec, result));
fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
fun set_result result =
- map_node (fn (touched, header, perspective, entries, _) =>
- (touched, header, perspective, entries, result));
+ map_node (fn (touched, header, perspective, entries, last_exec, _) =>
+ (touched, header, perspective, entries, last_exec, result));
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
fun default_node name = Graph.default_node (name, empty_node);
@@ -134,13 +139,26 @@
type edit = string * node_edit;
+fun after_entry (Node {entries, ...}) = Entries.get_after entries;
+
+fun lookup_entry (Node {entries, ...}) id =
+ (case Entries.lookup entries id of
+ NONE => NONE
+ | SOME (exec, _) => exec);
+
fun the_entry (Node {entries, ...}) id =
(case Entries.lookup entries id of
NONE => err_undef "command entry" id
- | SOME entry => entry);
+ | SOME (exec, _) => exec);
+
+fun the_default_entry node (SOME id) = the_default no_id (the_entry node id)
+ | the_default_entry _ NONE = no_id;
-fun update_entry (id, exec_id) =
- map_entries (Entries.update (id, SOME exec_id));
+fun update_entry id exec =
+ map_entries (Entries.update (id, exec));
+
+fun reset_entry id node =
+ if is_some (lookup_entry node id) then update_entry id NONE node else node;
fun reset_after id entries =
(case Entries.get_after entries id of
@@ -197,7 +215,9 @@
in Graph.map_node name (set_header header') nodes3 end
|> touch_node name
| Perspective perspective =>
- update_node name (set_perspective perspective) nodes);
+ nodes
+ |> update_node name (set_perspective perspective)
+ |> touch_node name (* FIXME more precise!?! *));
end;
@@ -254,7 +274,7 @@
val tr =
Future.fork_pri 2 (fn () =>
Position.setmp_thread_data (Position.id_only id_string)
- (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
+ (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
val commands' =
Inttab.update_new (id, tr) commands
handle Inttab.DUP dup => err_dup "command" dup;
@@ -344,7 +364,7 @@
-(** editing **)
+(** update **)
(* perspective *)
@@ -356,14 +376,32 @@
in define_version new_id new_version state end;
-(* edit *)
+(* edits *)
local
-fun is_changed node' ((_, id), exec) =
- (case try (the_entry node') id of
- NONE => true
- | SOME exec' => exec' <> exec);
+fun last_common last_visible node0 node =
+ let
+ fun get_common ((prev, id), exec) (found, (result, visible)) =
+ if found then NONE
+ else
+ let val found' = is_none exec orelse exec <> lookup_entry node0 id
+ in SOME (found', (prev, visible andalso prev <> last_visible)) end;
+ in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end;
+
+fun new_exec state init command_id' (execs, exec) =
+ let
+ val command' = the_command state command_id';
+ val exec_id' = new_id ();
+ val exec' =
+ snd exec |> Lazy.map (fn (st, _) =>
+ let val tr =
+ Future.join command'
+ |> Toplevel.modify_init init
+ |> Toplevel.put_id (print_id exec_id');
+ in run_command tr st end)
+ |> pair command_id';
+ in ((exec_id', exec') :: execs, exec') end;
fun init_theory deps name node =
let
@@ -379,65 +417,74 @@
SOME thy => thy
| NONE =>
get_theory (Position.file_only import)
- (#2 (Future.join (the (AList.lookup (op =) deps import))))));
+ (snd (Future.join (the (AList.lookup (op =) deps import))))));
in Thy_Load.begin_theory dir thy_name imports files parents end;
-fun new_exec state init command_id (assigns, execs, exec) =
- let
- val command = the_command state command_id;
- val exec_id' = new_id ();
- val exec' = exec |> Lazy.map (fn (st, _) =>
- let val tr =
- Future.join command
- |> Toplevel.modify_init init
- |> Toplevel.put_id (print_id exec_id');
- in run_command tr st end);
- in ((command_id, exec_id') :: assigns, (exec_id', (command_id, exec')) :: execs, exec') end;
-
in
-fun edit (old_id: version_id) (new_id: version_id) edits state =
+fun update (old_id: version_id) (new_id: version_id) edits state =
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 updates =
+ val updated =
nodes_of new_version |> Graph.schedule
(fn deps => fn (name, node) =>
if not (is_touched node) then Future.value (([], [], []), node)
else
- (case first_entry NONE (is_changed (node_of old_version name)) node of
- NONE => Future.value (([], [], []), set_touched false node)
- | SOME ((prev, id), _) =>
- let
- fun init () = init_theory deps name node;
- in
- (singleton o Future.forks)
- {name = "Document.edit", group = NONE,
- deps = map (Future.task_of o #2) deps, pri = 0, 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, last_exec) =
- fold_entries (SOME id) (new_exec state init o #2 o #1)
- node ([], [], #2 (the_exec state prev_exec));
- val node' = node
- |> fold update_entry assigns
- |> set_result (Lazy.map #1 last_exec)
- |> set_touched false;
- in ((assigns, execs, [(name, node')]), node') end)
- end))
+ let
+ val node0 = node_of old_version name;
+ fun init () = init_theory deps name node;
+ in
+ (singleton o Future.forks)
+ {name = "Document.update", group = NONE,
+ deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false}
+ (fn () =>
+ let
+ val last_visible = #2 (get_perspective node);
+ val (common, visible) = last_common last_visible node0 node;
+ val common_exec = the_exec state (the_default_entry node common);
+
+ val (execs, exec) = ([], common_exec) |>
+ visible ?
+ iterate_entries (after_entry node common)
+ (fn ((prev, id), _) => fn res =>
+ if prev = last_visible then NONE
+ else SOME (new_exec state init id res)) node;
+
+ val no_execs =
+ iterate_entries (after_entry node0 common)
+ (fn ((_, id0), exec0) => fn res =>
+ if is_none exec0 then NONE
+ else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res
+ else SOME (id0 :: res)) node0 [];
+
+ val last_exec = if #1 exec = no_id then NONE else SOME (#1 exec);
+ val result =
+ if is_some (after_entry node last_exec) then no_result
+ else Lazy.map #1 (#2 exec);
+
+ val node' = node
+ |> fold reset_entry no_execs
+ |> fold (fn (exec_id, (id, _)) => update_entry id (SOME exec_id)) execs
+ |> set_last_exec last_exec
+ |> set_result result
+ |> set_touched false;
+ in ((no_execs, execs, [(name, node')]), node') end)
+ end)
|> Future.joins |> map #1;
+ val command_execs =
+ map (rpair NONE) (maps #1 updated) @
+ map (fn (exec_id, (command_id, _)) => (command_id, SOME exec_id)) (maps #2 updated);
+ val updated_nodes = maps #3 updated;
+ val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes;
+
val state' = state
- |> fold (fold define_exec o #2) updates
- |> define_version new_id (fold (fold put_node o #3) updates new_version);
-
- in (maps #1 (rev updates), state') end;
+ |> fold (fold define_exec o #2) updated
+ |> define_version new_id (fold put_node updated_nodes new_version);
+ in ((command_execs, last_execs), state') end;
end;
@@ -467,7 +514,7 @@
(singleton o Future.forks)
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)),
deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true}
- (fold_entries NONE (fn (_, exec) => fn () => force_exec node exec) node));
+ (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node));
in (versions, commands, execs, execution) end);
--- a/src/Pure/PIDE/document.scala Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/PIDE/document.scala Fri Aug 26 15:11:33 2011 -0700
@@ -60,7 +60,8 @@
case exn => exn
}
- val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
+ val empty: Node =
+ Node(Exn.Exn(ERROR("Bad theory header")), Command.Perspective.empty, Map(), Linear_Set())
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
: Iterator[(Command, Text.Offset)] =
@@ -156,7 +157,7 @@
object Change
{
- val init = Change(Future.value(Version.init), Nil, Future.value(Version.init))
+ val init: Change = Change(Future.value(Version.init), Nil, Future.value(Version.init))
}
sealed case class Change(
@@ -172,7 +173,7 @@
object History
{
- val init = new History(List(Change.init))
+ val init: History = new History(List(Change.init))
}
// FIXME pruning, purging of state
@@ -203,21 +204,42 @@
: Stream[Text.Info[Option[A]]]
}
+ type Assign =
+ (List[(Document.Command_ID, Option[Document.Exec_ID])], // exec state assignment
+ List[(String, Option[Document.Command_ID])]) // last exec
+
+ val no_assign: Assign = (Nil, Nil)
+
object State
{
class Fail(state: State) extends Exception
- val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)._2
+ val init: State =
+ State().define_version(Version.init, Assignment.init).assign(Version.init.id, no_assign)._2
+
+ object Assignment
+ {
+ val init: Assignment = Assignment(Map.empty, Map.empty, false)
+ }
case class Assignment(
- val assignment: Map[Command, Exec_ID],
- val is_finished: Boolean = false)
+ val command_execs: Map[Command_ID, Exec_ID],
+ val last_execs: Map[String, Option[Command_ID]],
+ val is_finished: Boolean)
{
- def get_finished: Map[Command, Exec_ID] = { require(is_finished); assignment }
- def assign(command_execs: List[(Command, Exec_ID)]): Assignment =
+ def check_finished: Assignment = { require(is_finished); this }
+ def unfinished: Assignment = copy(is_finished = false)
+
+ def assign(add_command_execs: List[(Command_ID, Option[Exec_ID])],
+ add_last_execs: List[(String, Option[Command_ID])]): Assignment =
{
require(!is_finished)
- Assignment(assignment ++ command_execs, true)
+ val command_execs1 =
+ (command_execs /: add_command_execs) {
+ case (res, (command_id, None)) => res - command_id
+ case (res, (command_id, Some(exec_id))) => res + (command_id -> exec_id)
+ }
+ Assignment(command_execs1, last_execs ++ add_last_execs, true)
}
}
}
@@ -232,12 +254,12 @@
{
private def fail[A]: A = throw new State.Fail(this)
- def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State =
+ def define_version(version: Version, assignment: State.Assignment): State =
{
val id = version.id
if (versions.isDefinedAt(id) || disposed(id)) fail
copy(versions = versions + (id -> version),
- assignments = assignments + (id -> State.Assignment(former_assignment)))
+ assignments = assignments + (id -> assignment.unfinished))
}
def define_command(command: Command): State =
@@ -250,7 +272,7 @@
def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
- def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
+ def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) // FIXME rename
def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
def the_assignment(version: Version): State.Assignment =
assignments.getOrElse(version.id, fail)
@@ -269,21 +291,22 @@
}
}
- def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
+ def assign(id: Version_ID, arg: Assign): (List[Command], State) =
{
val version = the_version(id)
+ val (command_execs, last_execs) = arg
- var new_execs = execs
- val assigned_execs =
- for ((cmd_id, exec_id) <- edits) yield {
- val st = the_command(cmd_id)
- if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
- new_execs += (exec_id -> st)
- (st.command, exec_id)
+ val (commands, new_execs) =
+ ((Nil: List[Command], execs) /: command_execs) {
+ case ((commands1, execs1), (cmd_id, Some(exec_id))) =>
+ val st = the_command(cmd_id)
+ (st.command :: commands1, execs1 + (exec_id -> st))
+ case (res, (_, None)) => res
}
- val new_assignment = the_assignment(version).assign(assigned_execs)
+ val new_assignment = the_assignment(version).assign(command_execs, last_execs)
val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs)
- (assigned_execs.map(_._1), new_state)
+
+ (commands, new_state)
}
def is_assigned(version: Version): Boolean =
@@ -295,8 +318,24 @@
def is_stable(change: Change): Boolean =
change.is_finished && is_assigned(change.version.get_finished)
+ def recent_stable: Option[Change] = history.undo_list.find(is_stable)
def tip_stable: Boolean = is_stable(history.tip)
- def recent_stable: Option[Change] = history.undo_list.find(is_stable)
+ def tip_version: Version = history.tip.version.get_finished
+
+ def last_exec_offset(name: String): Text.Offset =
+ {
+ val version = tip_version
+ the_assignment(version).last_execs.get(name) match {
+ case Some(Some(id)) =>
+ val node = version.nodes(name)
+ val cmd = the_command(id).command
+ node.command_start(cmd) match {
+ case None => 0
+ case Some(start) => start + cmd.length
+ }
+ case _ => 0
+ }
+ }
def continue_history(
previous: Future[Version],
@@ -329,7 +368,10 @@
def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
def state(command: Command): Command.State =
- try { the_exec(the_assignment(version).get_finished.getOrElse(command, fail)) }
+ try {
+ the_exec(the_assignment(version).check_finished.command_execs
+ .getOrElse(command.id, fail))
+ }
catch { case _: State.Fail => command.empty_state }
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
--- a/src/Pure/PIDE/isar_document.ML Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/PIDE/isar_document.ML Fri Aug 26 15:11:33 2011 -0700
@@ -28,7 +28,7 @@
end));
val _ =
- Isabelle_Process.add_command "Isar_Document.edit_version"
+ Isabelle_Process.add_command "Isar_Document.update"
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
let
val old_id = Document.parse_id old_id_string;
@@ -48,12 +48,15 @@
end;
val running = Document.cancel_execution state;
- val (updates, state') = Document.edit old_id new_id edits state;
+ val (assignment, state') = Document.update old_id new_id edits state;
val _ = Future.join_tasks running;
val _ = Document.join_commands state';
val _ =
Output.status (Markup.markup (Markup.assign new_id)
- (implode (map (Markup.markup_only o Markup.edit) updates)));
+ (assignment |>
+ let open XML.Encode
+ in pair (list (pair int (option int))) (list (pair string (option int))) end
+ |> YXML.string_of_body));
val state'' = Document.execute new_id state';
in state'' end));
--- a/src/Pure/PIDE/isar_document.scala Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/PIDE/isar_document.scala Fri Aug 26 15:11:33 2011 -0700
@@ -11,24 +11,20 @@
{
/* document editing */
- object Assign {
- def unapply(msg: XML.Tree)
- : Option[(Document.Version_ID, List[(Document.Command_ID, Document.Exec_ID)])] =
+ object Assign
+ {
+ def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
msg match {
- case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), edits) =>
- val id_edits = edits.map(Edit.unapply)
- if (id_edits.forall(_.isDefined)) Some((id, id_edits.map(_.get)))
- else None
- case _ => None
- }
- }
-
- object Edit {
- def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] =
- msg match {
- case XML.Elem(
- Markup(Markup.EDIT,
- List((Markup.ID, Document.ID(i)), (Markup.EXEC, Document.ID(j)))), Nil) => Some((i, j))
+ case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
+ try {
+ import XML.Decode._
+ val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body)
+ Some(id, a)
+ }
+ catch {
+ case _: XML.XML_Atom => None
+ case _: XML.XML_Body => None
+ }
case _ => None
}
}
@@ -144,13 +140,13 @@
{
val ids =
{ import XML.Encode._
- list(long)(perspective.map(_.id)) }
+ list(long)(perspective.commands.map(_.id)) }
input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
YXML.string_of_body(ids))
}
- def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
edits: List[Document.Edit_Command])
{
val edits_yxml =
@@ -164,10 +160,10 @@
{ case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
(Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
{ case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
- { case Document.Node.Perspective(cs) => (cs.map(c => long_atom(c.id)), Nil) }))))
+ { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))))
YXML.string_of_body(encode(edits)) }
- input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
+ input("Isar_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
}
--- a/src/Pure/PIDE/text.scala Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/PIDE/text.scala Fri Aug 26 15:11:33 2011 -0700
@@ -62,28 +62,39 @@
/* perspective */
- type Perspective = List[Range] // visible text partitioning in canonical order
-
- def perspective(ranges: Seq[Range]): Perspective =
+ object Perspective
{
- val sorted_ranges = ranges.toArray
- Sorting.quickSort(sorted_ranges)(Range.Ordering)
+ val empty: Perspective = Perspective(Nil)
- val result = new mutable.ListBuffer[Text.Range]
- var last: Option[Text.Range] = None
- for (range <- sorted_ranges)
+ def apply(ranges: Seq[Range]): Perspective =
{
- last match {
- case Some(last_range)
- if ((last_range overlaps range) || last_range.stop == range.start) =>
- last = Some(Text.Range(last_range.start, range.stop))
- case _ =>
- result ++= last
- last = Some(range)
+ val sorted_ranges = ranges.toArray
+ Sorting.quickSort(sorted_ranges)(Range.Ordering)
+
+ val result = new mutable.ListBuffer[Text.Range]
+ var last: Option[Text.Range] = None
+ for (range <- sorted_ranges)
+ {
+ last match {
+ case Some(last_range)
+ if ((last_range overlaps range) || last_range.stop == range.start) =>
+ last = Some(Text.Range(last_range.start, range.stop))
+ case _ =>
+ result ++= last
+ last = Some(range)
+ }
}
+ result ++= last
+ new Perspective(result.toList)
}
- result ++= last
- result.toList
+ }
+
+ sealed case class Perspective(ranges: List[Range]) // visible text partitioning in canonical order
+ {
+ def is_empty: Boolean = ranges.isEmpty
+ def range: Range =
+ if (is_empty) Range(0)
+ else Range(ranges.head.start, ranges.last.stop)
}
--- a/src/Pure/Syntax/syntax_ext.ML Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Aug 26 15:11:33 2011 -0700
@@ -231,8 +231,8 @@
val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
val args = filter (fn Argument _ => true | _ => false) raw_symbs;
- val (const', typ', parse_rules) =
- if not (exists is_index args) then (const, typ, [])
+ val (const', typ', syntax_consts, parse_rules) =
+ if not (exists is_index args) then (const, typ, NONE, NONE)
else
let
val indexed_const =
@@ -247,7 +247,7 @@
val lhs = Ast.mk_appl (Ast.Constant indexed_const)
(xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
- in (indexed_const, rangeT, [(lhs, rhs)]) end;
+ in (indexed_const, rangeT, SOME (indexed_const, const), SOME (lhs, rhs)) end;
val (symbs, lhs) = add_args raw_symbs typ' pris;
@@ -273,7 +273,7 @@
else if exists is_terminal symbs' then xprod
else XProd (lhs', map rem_pri symbs', "", chain_pri);
- in (xprod', parse_rules) end;
+ in (xprod', syntax_consts, parse_rules) end;
@@ -298,13 +298,15 @@
val (parse_ast_translation, parse_translation, print_translation,
print_ast_translation) = trfuns;
- val (xprods, parse_rules') = map (mfix_to_xprod is_logtype) mfixes
- |> split_list |> apsnd (rev o flat);
+ val xprod_results = map (mfix_to_xprod is_logtype) mfixes;
+ val xprods = map #1 xprod_results;
+ val consts' = map_filter #2 xprod_results;
+ val parse_rules' = rev (map_filter #3 xprod_results);
val mfix_consts = map (fn Mfix x => (#3 x, "")) mfixes @ map (fn XProd x => (#3 x, "")) xprods;
in
Syn_Ext {
xprods = xprods,
- consts = mfix_consts @ consts,
+ consts = mfix_consts @ consts' @ consts,
parse_ast_translation = parse_ast_translation,
parse_rules = parse_rules' @ parse_rules,
parse_translation = parse_translation,
--- a/src/Pure/System/session.scala Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/System/session.scala Fri Aug 26 15:11:33 2011 -0700
@@ -206,7 +206,7 @@
def update_perspective(name: String, text_perspective: Text.Perspective)
{
- val previous = global_state().history.tip.version.get_finished
+ val previous = global_state().tip_version
val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
val text_edits: List[Document.Edit_Text] =
@@ -215,9 +215,9 @@
global_state.change_yield(
_.continue_history(Future.value(previous), text_edits, Future.value(version)))
- val assignment = global_state().the_assignment(previous).get_finished
+ val assignment = global_state().the_assignment(previous).check_finished
global_state.change(_.define_version(version, assignment))
- global_state.change_yield(_.assign(version.id, Nil))
+ global_state.change_yield(_.assign(version.id, Document.no_assign))
prover.get.update_perspective(previous.id, version.id, name, perspective)
}
@@ -248,10 +248,10 @@
/* exec state assignment */
- def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)])
+ def handle_assign(id: Document.Version_ID, assign: Document.Assign)
//{{{
{
- val cmds = global_state.change_yield(_.assign(id, edits))
+ val cmds = global_state.change_yield(_.assign(id, assign))
for (cmd <- cmds) command_change_buffer ! cmd
assignments.event(Session.Assignment)
}
@@ -268,13 +268,6 @@
val name = change.name
val doc_edits = change.doc_edits
- var former_assignment = global_state().the_assignment(previous).get_finished
- for {
- (name, Document.Node.Edits(cmd_edits)) <- doc_edits // FIXME proper coverage!?
- (prev, None) <- cmd_edits
- removed <- previous.nodes(name).commands.get_after(prev)
- } former_assignment -= removed
-
def id_command(command: Command)
{
if (global_state().lookup_command(command.id).isEmpty) {
@@ -287,8 +280,9 @@
edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
}
- global_state.change(_.define_version(version, former_assignment))
- prover.get.edit_version(previous.id, version.id, doc_edits)
+ val assignment = global_state().the_assignment(previous).check_finished
+ global_state.change(_.define_version(version, assignment))
+ prover.get.update(previous.id, version.id, doc_edits)
}
//}}}
@@ -336,8 +330,8 @@
else if (result.is_stdout) { }
else if (result.is_status) {
result.body match {
- case List(Isar_Document.Assign(id, edits)) =>
- try { handle_assign(id, edits) }
+ case List(Isar_Document.Assign(id, assign)) =>
+ try { handle_assign(id, assign) }
catch { case _: Document.State.Fail => bad_result(result) }
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
@@ -386,7 +380,8 @@
reply(())
case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
- if (text_edits.isEmpty && global_state().tip_stable)
+ if (text_edits.isEmpty && global_state().tip_stable &&
+ perspective.range.stop <= global_state().last_exec_offset(name))
update_perspective(name, perspective)
else
handle_edits(name, master_dir, header,
--- a/src/Pure/Thy/thy_load.ML Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/Thy/thy_load.ML Fri Aug 26 15:11:33 2011 -0700
@@ -175,7 +175,7 @@
val spans = Source.exhaust (Thy_Syntax.span_source toks);
val elements =
Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
- |> maps (Outer_Syntax.prepare_element outer_syntax init);
+ |> maps (Outer_Syntax.read_element outer_syntax init);
val _ = Present.theory_source name
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
--- a/src/Pure/Thy/thy_syntax.scala Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.scala Fri Aug 26 15:11:33 2011 -0700
@@ -101,7 +101,7 @@
def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
{
- if (perspective.isEmpty) Nil
+ if (perspective.is_empty) Command.Perspective.empty
else {
val result = new mutable.ListBuffer[Command]
@tailrec
@@ -120,9 +120,8 @@
case _ =>
}
}
- val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
- check_ranges(perspective, node.command_range(perspective_range).toStream)
- result.toList
+ check_ranges(perspective.ranges, node.command_range(perspective.range).toStream)
+ Command.Perspective(result.toList)
}
}
@@ -132,7 +131,7 @@
val node = nodes(name)
val perspective = command_perspective(node, text_perspective)
val new_nodes =
- if (Command.equal_perspective(node.perspective, perspective)) None
+ if (node.perspective same perspective) None
else Some(nodes + (name -> node.copy(perspective = perspective)))
(perspective, new_nodes)
}
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Tools/jEdit/lib/Tools/jedit Fri Aug 26 15:11:33 2011 -0700
@@ -134,11 +134,14 @@
# args
-while [ "$#" -gt 0 ]
-do
- ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
- shift
-done
+if [ "$#" -eq 0 ]; then
+ ARGS["${#ARGS[@]}"]="Scratch.thy"
+else
+ while [ "$#" -gt 0 ]; do
+ ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+ shift
+ done
+fi
## dependencies
--- a/src/Tools/jEdit/src/document_model.scala Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Tools/jEdit/src/document_model.scala Fri Aug 26 15:11:33 2011 -0700
@@ -74,10 +74,10 @@
def perspective(): Text.Perspective =
{
Swing_Thread.require()
- Text.perspective(
+ Text.Perspective(
for {
doc_view <- Isabelle.document_views(buffer)
- range <- doc_view.perspective()
+ range <- doc_view.perspective().ranges
} yield range)
}
@@ -88,7 +88,7 @@
{
private val pending = new mutable.ListBuffer[Text.Edit]
private var pending_perspective = false
- private var last_perspective: Text.Perspective = Nil
+ private var last_perspective: Text.Perspective = Text.Perspective.empty
def snapshot(): List[Text.Edit] = pending.toList
@@ -101,7 +101,7 @@
else last_perspective
snapshot() match {
- case Nil if new_perspective == last_perspective =>
+ case Nil if last_perspective == new_perspective =>
case edits =>
pending.clear
last_perspective = new_perspective
--- a/src/Tools/jEdit/src/document_view.scala Fri Aug 26 15:11:26 2011 -0700
+++ b/src/Tools/jEdit/src/document_view.scala Fri Aug 26 15:11:33 2011 -0700
@@ -118,7 +118,7 @@
def perspective(): Text.Perspective =
{
Swing_Thread.require()
- Text.perspective(
+ Text.Perspective(
for {
i <- 0 until text_area.getVisibleLines
val start = text_area.getScreenLineStartOffset(i)