--- a/src/HOL/Groups.thy Wed Aug 24 15:25:39 2011 +0200
+++ b/src/HOL/Groups.thy Wed Aug 24 17:30:25 2011 +0200
@@ -103,11 +103,6 @@
hide_const (open) zero one
-syntax
- "_index1" :: index ("\<^sub>1")
-translations
- (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
lemma Let_0 [simp]: "Let 0 f = f 0"
unfolding Let_def ..
--- a/src/Pure/General/timing.ML Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Pure/General/timing.ML Wed Aug 24 17:30:25 2011 +0200
@@ -20,6 +20,7 @@
val start: unit -> start
val result: start -> timing
val timing: ('a -> 'b) -> 'a -> timing * 'b
+ val is_relevant: timing -> bool
val message: timing -> string
end
@@ -67,11 +68,6 @@
(* timing messages *)
-fun message {elapsed, cpu, gc} =
- Time.toString elapsed ^ "s elapsed time, " ^
- Time.toString cpu ^ "s cpu time, " ^
- Time.toString gc ^ "s GC time" handle Time.Time => "";
-
val min_time = Time.fromMilliseconds 1;
fun is_relevant {elapsed, cpu, gc} =
@@ -79,6 +75,11 @@
Time.>= (cpu, min_time) orelse
Time.>= (gc, min_time);
+fun message {elapsed, cpu, gc} =
+ Time.toString elapsed ^ "s elapsed time, " ^
+ Time.toString cpu ^ "s cpu time, " ^
+ Time.toString gc ^ "s GC time" handle Time.Time => "";
+
fun cond_timeit enabled msg e =
if enabled then
let
--- a/src/Pure/PIDE/document.ML Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Pure/PIDE/document.ML Wed Aug 24 17:30:25 2011 +0200
@@ -24,9 +24,10 @@
type edit = string * node_edit
type state
val init_state: state
+ val define_command: command_id -> string -> state -> state
val join_commands: state -> unit
val cancel_execution: state -> Future.task list
- val define_command: command_id -> string -> state -> state
+ 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 execute: version_id -> state -> state
val state: unit -> state
@@ -61,50 +62,62 @@
structure Entries = Linear_Set(type key = command_id val ord = int_ord);
abstype node = Node of
- {header: node_header,
+ {touched: bool,
+ header: node_header,
perspective: perspective,
entries: exec_id option Entries.T, (*command entries with excecutions*)
result: Toplevel.state lazy}
and version = Version of node Graph.T (*development graph wrt. static imports*)
with
-fun make_node (header, perspective, entries, result) =
- Node {header = header, perspective = perspective, entries = entries, result = result};
+fun make_node (touched, header, perspective, entries, result) =
+ Node {touched = touched, header = header, perspective = perspective,
+ entries = entries, result = result};
-fun map_node f (Node {header, perspective, entries, result}) =
- make_node (f (header, perspective, entries, result));
+fun map_node f (Node {touched, header, perspective, entries, result}) =
+ make_node (f (touched, header, perspective, entries, result));
-val no_perspective: perspective = (K false, []);
+fun make_perspective ids : perspective =
+ (Inttab.defined (Inttab.make (map (rpair ()) ids)), ids);
+
+val no_perspective = make_perspective [];
val no_print = Lazy.value ();
val no_result = Lazy.value Toplevel.toplevel;
val empty_node =
- make_node (Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
+ make_node (false, Exn.Exn (ERROR "Bad theory header"), no_perspective, Entries.empty, no_result);
val clear_node =
- map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, no_result));
+ map_node (fn (_, header, _, _, _) => (false, header, no_perspective, Entries.empty, 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));
+
fun get_header (Node {header, ...}) = header;
fun set_header header =
- map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
+ map_node (fn (touched, _, perspective, entries, result) =>
+ (touched, header, perspective, entries, result));
fun get_perspective (Node {perspective, ...}) = perspective;
-fun set_perspective perspective =
- let val pred = Inttab.defined (Inttab.make (map (rpair ()) perspective)) in
- map_node (fn (header, _, entries, result) => (header, (pred, perspective), entries, result))
- end;
+fun set_perspective ids =
+ map_node (fn (touched, header, _, entries, result) =>
+ (touched, header, make_perspective ids, entries, result));
-fun map_entries f (Node {header, perspective, entries, result}) =
- make_node (header, perspective, f entries, 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;
fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.force result);
fun set_result result =
- map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
+ map_node (fn (touched, header, perspective, entries, _) =>
+ (touched, header, perspective, entries, 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);
@@ -146,35 +159,47 @@
fun nodes_of (Version nodes) = nodes;
val node_of = get_node o nodes_of;
+local
+
fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
-fun touch_descendants name nodes =
- fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE)))
+fun touch_node name nodes =
+ fold (fn desc =>
+ update_node desc (set_touched true) #>
+ desc <> name ? update_node desc (map_entries (reset_after NONE)))
(Graph.all_succs nodes [name]) nodes;
+in
+
fun edit_nodes (name, node_edit) (Version nodes) =
Version
- (touch_descendants name
- (case node_edit of
- Clear => update_node name clear_node nodes
- | Edits edits =>
- nodes
- |> update_node name (edit_node edits)
- | Header header =>
- let
- val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
- val nodes1 = nodes
- |> default_node name
- |> fold default_node parents;
- val nodes2 = nodes1
- |> Graph.Keys.fold
- (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
- val (header', nodes3) =
- (header, Graph.add_deps_acyclic (name, parents) nodes2)
- handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
- in Graph.map_node name (set_header header') nodes3 end
- | Perspective perspective =>
- update_node name (set_perspective perspective) nodes));
+ (case node_edit of
+ Clear =>
+ nodes
+ |> update_node name clear_node
+ |> touch_node name
+ | Edits edits =>
+ nodes
+ |> update_node name (edit_node edits)
+ |> touch_node name
+ | Header header =>
+ let
+ val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
+ val nodes1 = nodes
+ |> default_node name
+ |> fold default_node parents;
+ val nodes2 = nodes1
+ |> Graph.Keys.fold
+ (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
+ val (header', nodes3) =
+ (header, Graph.add_deps_acyclic (name, parents) nodes2)
+ handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
+ in Graph.map_node name (set_header header') nodes3 end
+ |> touch_node name
+ | Perspective perspective =>
+ update_node name (set_perspective perspective) nodes);
+
+end;
fun put_node (name, node) (Version nodes) =
Version (update_node name (K node) nodes);
@@ -270,7 +295,8 @@
local
-fun timing tr t = Toplevel.status tr (Markup.timing t);
+fun timing tr t =
+ if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else ();
fun proof_status tr st =
(case try Toplevel.proof_of st of
@@ -320,6 +346,16 @@
(** editing **)
+(* perspective *)
+
+fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state =
+ let
+ val old_version = the_version state old_id;
+ val _ = Time.now (); (* FIXME odd workaround for polyml-5.4.0/x86_64 -- needed? *)
+ val new_version = edit_nodes (name, Perspective perspective) old_version;
+ in define_version new_id new_version state end;
+
+
(* edit *)
local
@@ -329,11 +365,32 @@
NONE => true
| SOME exec' => exec' <> exec);
-fun new_exec (command_id, command) (assigns, execs, exec) =
+fun init_theory deps name node =
let
+ val (thy_name, imports, uses) = Exn.release (get_header node);
+ (* FIXME provide files via Scala layer *)
+ val (dir, files) =
+ if ML_System.platform_is_cygwin then (Path.current, [])
+ else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
+
+ val parents =
+ imports |> map (fn import =>
+ (case Thy_Info.lookup_theory import of (* FIXME more robust!? *)
+ SOME thy => thy
+ | NONE =>
+ get_theory (Position.file_only import)
+ (#2 (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 = Toplevel.put_id (print_id exec_id') (Future.join command)
+ 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;
@@ -348,46 +405,32 @@
val updates =
nodes_of new_version |> Graph.schedule
(fn deps => fn (name, node) =>
- (case first_entry NONE (is_changed (node_of old_version name)) node of
- NONE => Future.value (([], [], []), node)
- | SOME ((prev, id), _) =>
- let
- fun init () =
- let
- val (thy_name, imports, uses) = Exn.release (get_header node);
- (* FIXME provide files via Scala layer *)
- val (dir, files) =
- if ML_System.platform_is_cygwin then (Path.current, [])
- else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
-
- val parents =
- imports |> map (fn import =>
- (case Thy_Info.lookup_theory import of
- SOME thy => thy
- | NONE =>
- get_theory (Position.file_only import)
- (#2 (Future.join (the (AList.lookup (op =) deps import))))));
- in Thy_Load.begin_theory dir thy_name imports files parents end;
- fun get_command id =
- (id, the_command state id |> Future.map (Toplevel.modify_init init));
- in
- (singleton o Future.forks)
- {name = "Document.edit", group = NONE,
- deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false}
- (fn () =>
- let
- val prev_exec =
- (case prev of
- NONE => no_id
- | SOME prev_id => the_default no_id (the_entry node prev_id));
- val (assigns, execs, last_exec) =
- fold_entries (SOME id) (new_exec o get_command 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);
- in ((assigns, execs, [(name, node')]), node') end)
- end))
+ 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))
|> Future.joins |> map #1;
val state' = state
@@ -411,9 +454,8 @@
let
val (command_id, exec) = the_exec state exec_id;
val (_, print) = Lazy.force exec;
- val perspective = get_perspective node;
val _ =
- if #1 (get_perspective node) command_id orelse true (* FIXME *)
+ if #1 (get_perspective node) command_id
then ignore (Lazy.future Future.default_params print)
else ();
in () end;
--- a/src/Pure/PIDE/document.scala Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Pure/PIDE/document.scala Wed Aug 24 17:30:25 2011 +0200
@@ -54,11 +54,10 @@
case class Header[A, B](header: Node_Header) extends Edit[A, B]
case class Perspective[A, B](perspective: B) extends Edit[A, B]
- def norm_header[A, B](f: String => String, g: String => String, header: Node_Header)
- : Header[A, B] =
+ def norm_header(f: String => String, g: String => String, header: Node_Header): Node_Header =
header match {
- case Exn.Res(h) => Header[A, B](Exn.capture { h.norm_deps(f, g) })
- case exn => Header[A, B](exn)
+ case Exn.Res(h) => Exn.capture { h.norm_deps(f, g) }
+ case exn => exn
}
val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
@@ -83,6 +82,9 @@
val blobs: Map[String, Blob],
val commands: Linear_Set[Command])
{
+ def clear: Node = Node.empty.copy(header = header)
+
+
/* commands */
private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
@@ -146,7 +148,8 @@
val init: Version = Version(no_id, Map().withDefaultValue(Node.empty))
}
- sealed case class Version(val id: Version_ID, val nodes: Map[String, Node])
+ type Nodes = Map[String, Node]
+ sealed case class Version(val id: Version_ID, val nodes: Nodes)
/* changes of plain text, eventually resulting in document edits */
@@ -221,8 +224,8 @@
sealed case class State(
val versions: Map[Version_ID, Version] = Map(),
- val commands: Map[Command_ID, Command.State] = Map(),
- val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
+ val commands: Map[Command_ID, Command.State] = Map(), // static markup from define_command
+ val execs: Map[Exec_ID, Command.State] = Map(), // dynamic markup from execution
val assignments: Map[Version_ID, State.Assignment] = Map(),
val disposed: Set[ID] = Set(), // FIXME unused!?
val history: History = History.init)
@@ -248,15 +251,15 @@
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_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
+ def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
def the_assignment(version: Version): State.Assignment =
assignments.getOrElse(version.id, fail)
def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
- case Some((st, occs)) =>
+ case Some(st) =>
val new_st = st.accumulate(message)
- (new_st, copy(execs = execs + (id -> (new_st, occs))))
+ (new_st, copy(execs = execs + (id -> new_st)))
case None =>
commands.get(id) match {
case Some(st) =>
@@ -269,14 +272,13 @@
def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): (List[Command], State) =
{
val version = the_version(id)
- val occs = Set(version) // FIXME unused (!?)
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, occs))
+ new_execs += (exec_id -> st)
(st.command, exec_id)
}
val new_assignment = the_assignment(version).assign(assigned_execs)
@@ -290,7 +292,14 @@
case None => false
}
- def extend_history(previous: Future[Version],
+ def is_stable(change: Change): Boolean =
+ change.is_finished && is_assigned(change.version.get_finished)
+
+ def tip_stable: Boolean = is_stable(history.tip)
+ def recent_stable: Option[Change] = history.undo_list.find(is_stable)
+
+ def continue_history(
+ previous: Future[Version],
edits: List[Edit_Text],
version: Future[Version]): (Change, State) =
{
@@ -302,11 +311,8 @@
// persistent user-view
def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
{
- val found_stable = history.undo_list.find(change =>
- change.is_finished && is_assigned(change.version.get_finished))
- require(found_stable.isDefined)
- val stable = found_stable.get
- val latest = history.undo_list.head
+ val stable = recent_stable.get
+ val latest = history.tip
// FIXME proper treatment of removed nodes
val edits =
@@ -323,7 +329,7 @@
def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
def state(command: Command): Command.State =
- try { the_exec_state(the_assignment(version).get_finished.getOrElse(command, fail)) }
+ try { the_exec(the_assignment(version).get_finished.getOrElse(command, 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 Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML Wed Aug 24 17:30:25 2011 +0200
@@ -12,6 +12,22 @@
(fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
val _ =
+ Isabelle_Process.add_command "Isar_Document.update_perspective"
+ (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state =>
+ let
+ val old_id = Document.parse_id old_id_string;
+ val new_id = Document.parse_id new_id_string;
+ val ids = YXML.parse_body ids_yxml
+ |> let open XML.Decode in list int end;
+
+ val _ = Future.join_tasks (Document.cancel_execution state);
+ in
+ state
+ |> Document.update_perspective old_id new_id name ids
+ |> Document.execute new_id
+ end));
+
+val _ =
Isabelle_Process.add_command "Isar_Document.edit_version"
(fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state =>
let
@@ -31,15 +47,15 @@
fn (a, []) => Document.Perspective (map int_atom a)]))
end;
- val running = Document.cancel_execution state;
- val (updates, state') = Document.edit 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)));
- val state'' = Document.execute new_id state';
- in state'' end));
+ val running = Document.cancel_execution state;
+ val (updates, state') = Document.edit 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)));
+ val state'' = Document.execute new_id state';
+ in state'' end));
val _ =
Isabelle_Process.add_command "Isar_Document.invoke_scala"
--- a/src/Pure/PIDE/isar_document.scala Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Wed Aug 24 17:30:25 2011 +0200
@@ -139,6 +139,17 @@
/* document versions */
+ def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ name: String, perspective: Command.Perspective)
+ {
+ val ids =
+ { import XML.Encode._
+ list(long)(perspective.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,
edits: List[Document.Edit_Command])
{
--- a/src/Pure/Syntax/syntax_trans.ML Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Wed Aug 24 17:30:25 2011 +0200
@@ -252,21 +252,22 @@
if 1 <= i andalso i <= length structs then nth structs (i - 1)
else error ("Illegal reference to implicit structure #" ^ string_of_int i);
-fun struct_tr structs [Const ("_indexdefault", _)] =
- Syntax.free (the_struct structs 1)
+fun legacy_struct structs i =
+ let
+ val x = the_struct structs i;
+ val _ =
+ legacy_feature
+ ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ string_of_int i) ^
+ Position.str_of (Position.thread_data ()) ^
+ " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
+ (if i = 1 then " (may be omitted)" else ""))
+ in x end;
+
+fun struct_tr structs [Const ("_indexdefault", _)] = Syntax.free (the_struct structs 1)
+ | struct_tr structs [Const ("_index1", _)] = Syntax.free (legacy_struct structs 1)
| struct_tr structs [t as (Const ("_indexnum", _) $ Const (s, _))] =
(case Lexicon.read_nat s of
- SOME n =>
- let
- val x = the_struct structs n;
- val advice =
- " -- use " ^ quote ("\\<^bsub>" ^ x ^ "\\<^esub>") ^ " instead" ^
- (if n = 1 then " (may be omitted)" else "");
- val _ =
- legacy_feature
- ("Old-style numbered structure index " ^ quote ("\\<^sub>" ^ s) ^
- Position.str_of (Position.thread_data ()) ^ advice);
- in Syntax.free x end
+ SOME i => Syntax.free (legacy_struct structs i)
| NONE => raise TERM ("struct_tr", [t]))
| struct_tr _ ts = raise TERM ("struct_tr", ts);
--- a/src/Pure/System/session.scala Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Pure/System/session.scala Wed Aug 24 17:30:25 2011 +0200
@@ -159,6 +159,28 @@
val thy_info = new Thy_Info(thy_load)
+ def header_edit(name: String, master_dir: String,
+ header: Document.Node_Header): Document.Edit_Text =
+ {
+ def norm_import(s: String): String =
+ {
+ val thy_name = Thy_Header.base_name(s)
+ if (thy_load.is_loaded(thy_name)) thy_name
+ else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
+ }
+ def norm_use(s: String): String =
+ file_store.append(master_dir, Path.explode(s))
+
+ val header1: Document.Node_Header =
+ header match {
+ case Exn.Res(Thy_Header(thy_name, _, _))
+ if (thy_load.is_loaded(thy_name)) =>
+ Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
+ case _ => Document.Node.norm_header(norm_import, norm_use, header)
+ }
+ (name, Document.Node.Header(header1))
+ }
+
/* actor messages */
@@ -180,6 +202,27 @@
var prover: Option[Isabelle_Process with Isar_Document] = None
+ /* perspective */
+
+ def update_perspective(name: String, text_perspective: Text.Perspective)
+ {
+ val previous = global_state().history.tip.version.get_finished
+ val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
+
+ val text_edits: List[Document.Edit_Text] =
+ List((name, Document.Node.Perspective(text_perspective)))
+ val change =
+ global_state.change_yield(
+ _.continue_history(Future.value(previous), text_edits, Future.value(version)))
+
+ val assignment = global_state().the_assignment(previous).get_finished
+ global_state.change(_.define_version(version, assignment))
+ global_state.change_yield(_.assign(version.id, Nil))
+
+ prover.get.update_perspective(previous.id, version.id, name, perspective)
+ }
+
+
/* incoming edits */
def handle_edits(name: String, master_dir: String,
@@ -189,20 +232,10 @@
val syntax = current_syntax()
val previous = global_state().history.tip.version
- def norm_import(s: String): String =
- {
- val name = Thy_Header.base_name(s)
- if (thy_load.is_loaded(name)) name
- else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
- }
- def norm_use(s: String): String = file_store.append(master_dir, Path.explode(s))
- val norm_header =
- Document.Node.norm_header[Text.Edit, Text.Perspective](norm_import, norm_use, header)
-
- val text_edits = (name, norm_header) :: edits.map(edit => (name, edit))
+ val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
val change =
- global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2)))
+ global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
result.map {
case (doc_edits, _) =>
@@ -213,6 +246,18 @@
//}}}
+ /* exec state assignment */
+
+ def handle_assign(id: Document.Version_ID, edits: List[(Document.Command_ID, Document.Exec_ID)])
+ //{{{
+ {
+ val cmds = global_state.change_yield(_.assign(id, edits))
+ for (cmd <- cmds) command_change_buffer ! cmd
+ assignments.event(Session.Assignment)
+ }
+ //}}}
+
+
/* resulting changes */
def handle_change(change: Change_Node)
@@ -292,11 +337,7 @@
else if (result.is_status) {
result.body match {
case List(Isar_Document.Assign(id, edits)) =>
- try {
- val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
- for (cmd <- cmds) command_change_buffer ! cmd
- assignments.event(Session.Assignment)
- }
+ try { handle_assign(id, edits) }
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
@@ -345,9 +386,11 @@
reply(())
case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
- handle_edits(name, master_dir, header,
- List(Document.Node.Edits(text_edits),
- Document.Node.Perspective(perspective)))
+ if (text_edits.isEmpty && global_state().tip_stable)
+ update_perspective(name, perspective)
+ else
+ handle_edits(name, master_dir, header,
+ List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
reply(())
case change: Change_Node if prover.isDefined =>
--- a/src/Pure/Thy/thy_syntax.scala Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Aug 24 17:30:25 2011 +0200
@@ -97,7 +97,7 @@
- /** command perspective **/
+ /** perspective **/
def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
{
@@ -126,6 +126,26 @@
}
}
+ def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective)
+ : (Command.Perspective, Option[Document.Nodes]) =
+ {
+ val node = nodes(name)
+ val perspective = command_perspective(node, text_perspective)
+ val new_nodes =
+ if (Command.equal_perspective(node.perspective, perspective)) None
+ else Some(nodes + (name -> node.copy(perspective = perspective)))
+ (perspective, new_nodes)
+ }
+
+ def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective)
+ : (Command.Perspective, Document.Version) =
+ {
+ val nodes = previous.nodes
+ val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
+ val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
+ (perspective, version)
+ }
+
/** text edits **/
@@ -212,7 +232,7 @@
edits foreach {
case (name, Document.Node.Clear()) =>
doc_edits += (name -> Document.Node.Clear())
- nodes -= name
+ nodes += (name -> nodes(name).clear)
case (name, Document.Node.Edits(text_edits)) =>
val node = nodes(name)
@@ -243,11 +263,11 @@
}
case (name, Document.Node.Perspective(text_perspective)) =>
- val node = nodes(name)
- val perspective = command_perspective(node, text_perspective)
- if (!Command.equal_perspective(node.perspective, perspective)) {
- doc_edits += (name -> Document.Node.Perspective(perspective))
- nodes += (name -> node.copy(perspective = perspective))
+ update_perspective(nodes, name, text_perspective) match {
+ case (_, None) =>
+ case (perspective, Some(nodes1)) =>
+ doc_edits += (name -> Document.Node.Perspective(perspective))
+ nodes = nodes1
}
}
(doc_edits.toList, Document.Version(Document.new_id(), nodes))
--- a/src/Pure/pure_thy.ML Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Pure/pure_thy.ML Wed Aug 24 17:30:25 2011 +0200
@@ -127,6 +127,7 @@
("_strip_positions", typ "'a", NoSyn),
("_constify", typ "num => num_const", Delimfix "_"),
("_constify", typ "float_token => float_const", Delimfix "_"),
+ ("_index1", typ "index", Delimfix "\\<^sub>1"),
("_indexnum", typ "num_const => index", Delimfix "\\<^sub>_"),
("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),
--- a/src/Tools/jEdit/src/document_model.scala Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Aug 24 17:30:25 2011 +0200
@@ -87,16 +87,25 @@
private object pending_edits // owned by Swing thread
{
private val pending = new mutable.ListBuffer[Text.Edit]
+ private var pending_perspective = false
+ private var last_perspective: Text.Perspective = Nil
+
def snapshot(): List[Text.Edit] = pending.toList
def flush()
{
Swing_Thread.require()
+
+ val new_perspective =
+ if (pending_perspective) { pending_perspective = false; perspective() }
+ else last_perspective
+
snapshot() match {
- case Nil =>
+ case Nil if new_perspective == last_perspective =>
case edits =>
pending.clear
- session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
+ last_perspective = new_perspective
+ session.edit_node(node_name, master_dir, node_header(), new_perspective, edits)
}
}
@@ -116,6 +125,18 @@
pending += edit
delay_flush()
}
+
+ def update_perspective()
+ {
+ pending_perspective = true
+ delay_flush()
+ }
+ }
+
+ def update_perspective()
+ {
+ Swing_Thread.require()
+ pending_edits.update_perspective()
}
--- a/src/Tools/jEdit/src/document_view.scala Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Aug 24 17:30:25 2011 +0200
@@ -25,7 +25,8 @@
import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
import org.gjt.sp.jedit.gui.RolloverButton
import org.gjt.sp.jedit.options.GutterOptionPane
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter,
+ ScrollListener}
import org.gjt.sp.jedit.syntax.{SyntaxStyle}
@@ -127,6 +128,16 @@
yield Text.Range(start, stop))
}
+ private def update_perspective = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ model.update_perspective()
+ }
+ }
+
/* snapshot */
@@ -467,6 +478,7 @@
private def activate()
{
val painter = text_area.getPainter
+ painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
text_area_painter.activate()
text_area.getGutter.addExtension(gutter_painter)
@@ -492,6 +504,7 @@
text_area.getGutter.removeExtension(gutter_painter)
text_area_painter.deactivate()
painter.removeExtension(tooltip_painter)
+ painter.removeExtension(update_perspective)
exit_popup()
}
}
--- a/src/Tools/jEdit/src/plugin.scala Wed Aug 24 15:25:39 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Aug 24 17:30:25 2011 +0200
@@ -409,7 +409,7 @@
Isabelle.start_session()
case msg: BufferUpdate
- if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
+ if msg.getWhat == BufferUpdate.LOADED =>
val buffer = msg.getBuffer
if (buffer != null && Isabelle.session.is_ready)