# HG changeset patch # User huffman # Date 1314396693 25200 # Node ID ddfd934e19bbab5f892e054fe303aaca5cec0301 # Parent 8037d25afa893781b3e51c6ffdb57360094368f4# Parent 534d7ee2644ac96fe4ec33165c9eea55036c6e16 merged diff -r 8037d25afa89 -r ddfd934e19bb src/HOL/Algebra/Congruence.thy --- 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 \ ((\x \ A. x .\\<^bsub>S\<^esub> B) \ (\x \ B. x .\\<^bsub>S\<^esub> A))" definition - eq_class_of :: "_ \ 'a \ 'a set" ("class'_of\ _") + eq_class_of :: "_ \ 'a \ 'a set" ("class'_of\") where "class_of\<^bsub>S\<^esub> x = {y \ carrier S. x .=\<^bsub>S\<^esub> y}" definition - eq_closure_of :: "_ \ 'a set \ 'a set" ("closure'_of\ _") + eq_closure_of :: "_ \ 'a set \ 'a set" ("closure'_of\") where "closure_of\<^bsub>S\<^esub> A = {y \ carrier S. y .\\<^bsub>S\<^esub> A}" definition - eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\ _") + eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\") where "is_closed\<^bsub>S\<^esub> A \ A \ carrier S \ closure_of\<^bsub>S\<^esub> A = A" abbreviation diff -r 8037d25afa89 -r ddfd934e19bb src/HOL/Algebra/Group.thy --- 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 \ Units G" "y \ carrier G" "z \ carrier G" then have "(inv x \ x) \ y = (inv x \ x) \ 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 \ Units G" "y \ carrier G" "z \ carrier G" @@ -332,7 +332,7 @@ proof - assume x: "x \ carrier G" then have "inv x \ (x \ inv x) = inv x \ \" - 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 \ carrier G" "y \ carrier G" then have "inv (x \ y) \ (x \ y) = (inv y \ inv x) \ (x \ 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 \ carrier G; H \ {}; \a \ H. inv a \ H; \a\H. \b\H. a \ b \ H |] ==> \ \ H" -by (force simp add: l_inv) +by force text {* A characterization of subgroups: closed, non-empty subset. *} diff -r 8037d25afa89 -r ddfd934e19bb src/HOL/Algebra/Lattice.thy --- 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]: "\ x .= y; y \ z; x \ carrier L; y \ carrier L; z \ carrier L \ \ x \ z" @@ -85,7 +86,7 @@ and yy': "y .= y'" and carr: "x \ carrier L" "y \ carrier L" "y' \ carrier L" shows "x \ 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 \ carrier ?L" diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/General/linear_set.ML --- 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 *) diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/General/markup.ML --- 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 *) diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/General/markup.scala --- 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 */ diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/Isar/outer_syntax.ML --- 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; diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/PIDE/command.scala --- 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 }) + } } } diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/PIDE/document.ML --- 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); diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/PIDE/document.scala --- 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)) diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/PIDE/isar_document.ML --- 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)); diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/PIDE/isar_document.scala --- 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) } diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/PIDE/text.scala --- 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) } diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/Syntax/syntax_ext.ML --- 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, diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/System/session.scala --- 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, diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/Thy/thy_load.ML --- 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); diff -r 8037d25afa89 -r ddfd934e19bb src/Pure/Thy/thy_syntax.scala --- 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) } diff -r 8037d25afa89 -r ddfd934e19bb src/Tools/jEdit/lib/Tools/jedit --- 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 diff -r 8037d25afa89 -r ddfd934e19bb src/Tools/jEdit/src/document_model.scala --- 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 diff -r 8037d25afa89 -r ddfd934e19bb src/Tools/jEdit/src/document_view.scala --- 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)