simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;
--- a/src/Pure/IsaMakefile Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Pure/IsaMakefile Thu Aug 05 14:35:35 2010 +0200
@@ -76,7 +76,7 @@
ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML \
- ML-Systems/use_context.ML Proof/extraction.ML \
+ ML-Systems/use_context.ML Proof/extraction.ML PIDE/document.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \
ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
--- a/src/Pure/Isar/isar_document.ML Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML Thu Aug 05 14:35:35 2010 +0200
@@ -1,7 +1,11 @@
(* Title: Pure/Isar/isar_document.ML
Author: Makarius
-Interactive Isar documents.
+Interactive Isar documents, which are structured as follows:
+
+ - history: tree of documents (i.e. changes without merge)
+ - document: graph of nodes (cf. theory files)
+ - node: linear set of commands, potentially with proof structure
*)
structure Isar_Document: sig end =
@@ -9,12 +13,6 @@
(* unique identifiers *)
-type state_id = string;
-type command_id = string;
-type document_id = string;
-
-val no_id = "";
-
local
val id_count = Synchronized.var "id" 0;
in
@@ -32,78 +30,84 @@
(** documents **)
+datatype entry = Entry of {next: Document.command_id option, state: Document.state_id option};
+type node = entry Symtab.table; (*unique command entries indexed by command_id, start with no_id*)
+type document = node Graph.T; (*development graph via static imports*)
+
+
(* command entries *)
-datatype entry = Entry of {next: command_id option, state: state_id option};
fun make_entry next state = Entry {next = next, state = state};
-fun the_entry entries (id: command_id) =
- (case Symtab.lookup entries id of
- NONE => err_undef "document entry" id
+fun the_entry (node: node) (id: Document.command_id) =
+ (case Symtab.lookup node id of
+ NONE => err_undef "command entry" id
| SOME (Entry entry) => entry);
-fun put_entry (id: command_id, entry: entry) = Symtab.update (id, entry);
+fun put_entry (id: Document.command_id, entry: entry) = Symtab.update (id, entry);
-fun put_entry_state (id: command_id) state entries =
- let val {next, ...} = the_entry entries id
- in put_entry (id, make_entry next state) entries end;
+fun put_entry_state (id: Document.command_id) state (node: node) =
+ let val {next, ...} = the_entry node id
+ in put_entry (id, make_entry next state) node end;
fun reset_entry_state id = put_entry_state id NONE;
fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id);
-(* document *)
-
-datatype document = Document of
- {dir: Path.T, (*master directory*)
- name: string, (*theory name*)
- entries: entry Symtab.table}; (*unique command entries indexed by command_id, start with no_id*)
-
-fun make_document dir name entries =
- Document {dir = dir, name = name, entries = entries};
-
-fun map_entries f (Document {dir, name, entries}) =
- make_document dir name (f entries);
-
-
(* iterate entries *)
-fun fold_entries id0 f (Document {entries, ...}) =
+fun fold_entries id0 f (node: node) =
let
fun apply NONE x = x
| apply (SOME id) x =
- let val entry = the_entry entries id
+ let val entry = the_entry node id
in apply (#next entry) (f (id, entry) x) end;
- in if Symtab.defined entries id0 then apply (SOME id0) else I end;
+ in if Symtab.defined node id0 then apply (SOME id0) else I end;
-fun first_entry P (Document {entries, ...}) =
+fun first_entry P (node: node) =
let
fun first _ NONE = NONE
| first prev (SOME id) =
- let val entry = the_entry entries id
+ let val entry = the_entry node id
in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end;
- in first NONE (SOME no_id) end;
+ in first NONE (SOME Document.no_id) end;
(* modify entries *)
-fun insert_after (id: command_id) (id2: command_id) = map_entries (fn entries =>
- let val {next, state} = the_entry entries id in
- entries
+fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) =
+ let val {next, state} = the_entry node id in
+ node
|> put_entry (id, make_entry (SOME id2) state)
|> put_entry (id2, make_entry next NONE)
- end);
+ end;
-fun delete_after (id: command_id) = map_entries (fn entries =>
- let val {next, state} = the_entry entries id in
+fun delete_after (id: Document.command_id) (node: node) =
+ let val {next, state} = the_entry node id in
(case next of
NONE => error ("No next entry to delete: " ^ quote id)
| SOME id2 =>
- entries |>
- (case #next (the_entry entries id2) of
+ node |>
+ (case #next (the_entry node id2) of
NONE => put_entry (id, make_entry NONE state)
| SOME id3 => put_entry (id, make_entry (SOME id3) state) #> reset_entry_state id3))
- end);
+ end;
+
+
+(* node operations *)
+
+val empty_node: node = Symtab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
+
+fun the_node (document: document) name =
+ Graph.get_node document name handle Graph.UNDEF _ => empty_node;
+
+fun edit_node (id, SOME id2) = insert_after id id2
+ | edit_node (id, NONE) = delete_after id;
+
+fun edit_nodes (name, NONE) = Graph.del_node name
+ | edit_nodes (name, SOME edits) =
+ Graph.default_node (name, empty_node) #>
+ Graph.map_node name (fold edit_node edits);
@@ -113,16 +117,17 @@
local
-val global_states = Unsynchronized.ref (Symtab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))]);
+val global_states =
+ Unsynchronized.ref (Symtab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]);
in
-fun define_state (id: state_id) state =
+fun define_state (id: Document.state_id) state =
NAMED_CRITICAL "Isar" (fn () =>
Unsynchronized.change global_states (Symtab.update_new (id, state))
handle Symtab.DUP dup => err_dup "state" dup);
-fun the_state (id: state_id) =
+fun the_state (id: Document.state_id) =
(case Symtab.lookup (! global_states) id of
NONE => err_undef "state" id
| SOME state => state);
@@ -134,16 +139,16 @@
local
-val global_commands = Unsynchronized.ref (Symtab.make [(no_id, Toplevel.empty)]);
+val global_commands = Unsynchronized.ref (Symtab.make [(Document.no_id, Toplevel.empty)]);
in
-fun define_command (id: command_id) tr =
+fun define_command (id: Document.command_id) tr =
NAMED_CRITICAL "Isar" (fn () =>
Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
handle Symtab.DUP dup => err_dup "command" dup);
-fun the_command (id: command_id) =
+fun the_command (id: Document.command_id) =
(case Symtab.lookup (! global_commands) id of
NONE => err_undef "command" id
| SOME tr => tr);
@@ -151,20 +156,20 @@
end;
-(* documents *)
+(* document versions *)
local
-val global_documents = Unsynchronized.ref (Symtab.empty: document Symtab.table);
+val global_documents = Unsynchronized.ref (Symtab.make [(Document.no_id, Graph.empty: document)]);
in
-fun define_document (id: document_id) document =
+fun define_document (id: Document.version_id) document =
NAMED_CRITICAL "Isar" (fn () =>
Unsynchronized.change global_documents (Symtab.update_new (id, document))
handle Symtab.DUP dup => err_dup "document" dup);
-fun the_document (id: document_id) =
+fun the_document (id: Document.version_id) =
(case Symtab.lookup (! global_documents) id of
NONE => err_undef "document" id
| SOME document => document);
@@ -175,41 +180,47 @@
(** main operations **)
-(* begin/end document *)
-
-val no_entries = Symtab.make [(no_id, make_entry NONE (SOME no_id))];
-
-fun begin_document (id: document_id) path =
- let
- val (dir, name) = Thy_Header.split_thy_path path;
- val _ = define_document id (make_document dir name no_entries);
- in () end;
-
-fun end_document (id: document_id) =
- NAMED_CRITICAL "Isar" (fn () =>
- let
- val document as Document {name, ...} = the_document id;
- val end_state =
- the_state (the (#state (#3 (the
- (first_entry (fn (_, {next, ...}) => is_none next) document)))));
- val _ = (* FIXME regular execution (??), result (??) *)
- Future.fork (fn () =>
- (case Lazy.force end_state of
- SOME st => Toplevel.end_theory (Position.id_only id) st
- | NONE => error ("Failed to finish theory " ^ quote name)));
- in () end);
-
-
-(* document editing *)
+(* execution *)
local
-fun is_changed entries' (id, {next = _, state}) =
- (case try (the_entry entries') id of
+val execution: unit future list Unsynchronized.ref = Unsynchronized.ref [];
+
+fun force_state NONE = ()
+ | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
+
+in
+
+fun execute document =
+ NAMED_CRITICAL "Isar" (fn () =>
+ let
+ val old_execution = ! execution;
+ val _ = List.app Future.cancel old_execution;
+ fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
+ (* FIXME proper node deps *)
+ val new_execution = Graph.keys document |> map (fn name =>
+ Future.fork_pri 1 (fn () =>
+ let
+ val _ = await_cancellation ();
+ val exec =
+ fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state)
+ (the_node document name);
+ in exec () end));
+ in execution := new_execution end);
+
+end;
+
+
+(* editing *)
+
+local
+
+fun is_changed node' (id, {next = _, state}) =
+ (case try (the_entry node') id of
NONE => true
| SOME {next = _, state = state'} => state' <> state);
-fun new_state name (id: command_id) (state_id, updates) =
+fun new_state name (id: Document.command_id) (state_id, updates) =
let
val state = the_state state_id;
val state_id' = create_id ();
@@ -227,46 +238,33 @@
|> Markup.markup Markup.assign
|> Output.status;
-
-fun force_state NONE = ()
- | force_state (SOME state_id) = ignore (Lazy.force (the_state state_id));
-
-val execution = Unsynchronized.ref (Future.value ());
-
-fun execute document =
- NAMED_CRITICAL "Isar" (fn () =>
- let
- val old_execution = ! execution;
- val _ = Future.cancel old_execution;
- val new_execution = Future.fork_pri 1 (fn () =>
- (uninterruptible (K Future.join_result) old_execution;
- fold_entries no_id (fn (_, {state, ...}) => fn () => force_state state) document ()));
- in execution := new_execution end);
-
in
-fun edit_document (old_id: document_id) (new_id: document_id) edits =
- NAMED_CRITICAL "Isar" (fn () =>
+fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
+ NAMED_CRITICAL "Isar" (fn () => exception_trace (fn () =>
let
- val old_document as Document {name, entries = old_entries, ...} = the_document old_id;
- val new_document as Document {entries = new_entries, ...} = old_document
- |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits;
+ val old_document = the_document old_id;
+ val new_document = fold edit_nodes edits old_document;
- val (updates, new_document') =
- (case first_entry (is_changed old_entries) new_document of
- NONE => ([], new_document)
+ fun update_node name node =
+ (case first_entry (is_changed (the_node old_document name)) node of
+ NONE => ([], node)
| SOME (prev, id, _) =>
let
- val prev_state_id = the (#state (the_entry new_entries (the prev)));
- val (_, updates) =
- fold_entries id (new_state name o #1) new_document (prev_state_id, []);
- val new_document' = new_document |> map_entries (fold set_entry_state updates);
- in (rev updates, new_document') end);
+ val prev_state_id = the (#state (the_entry node (the prev)));
+ val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
+ val node' = fold set_entry_state updates node;
+ in (rev updates, node') end);
+
+ (* FIXME proper node deps *)
+ val (updatess, new_document') =
+ (Graph.keys new_document, new_document)
+ |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
val _ = define_document new_id new_document';
- val _ = report_updates updates;
+ val _ = report_updates (flat updatess);
val _ = execute new_document';
- in () end);
+ in () end));
end;
@@ -282,21 +280,13 @@
define_command id (Outer_Syntax.prepare_command (Position.id id) text))));
val _ =
- Outer_Syntax.internal_command "Isar.begin_document"
- (Parse.string -- Parse.string >> (fn (id, path) =>
- Toplevel.imperative (fn () => begin_document id (Path.explode path))));
-
-val _ =
- Outer_Syntax.internal_command "Isar.end_document"
- (Parse.string >> (fn id => Toplevel.imperative (fn () => end_document id)));
-
-val _ =
Outer_Syntax.internal_command "Isar.edit_document"
(Parse.string -- Parse.string --
- Parse_Value.list (Parse.string -- (Parse.string >> SOME) || Parse.string >> rpair NONE)
- >> (fn ((id, new_id), edits) =>
- Toplevel.position (Position.id_only new_id) o
- Toplevel.imperative (fn () => edit_document id new_id edits)));
+ Parse_Value.list
+ (Parse.string -- Scan.option (Parse_Value.list (Parse.string -- Scan.option Parse.string)))
+ >> (fn ((old_id, new_id), edits) =>
+ Toplevel.position (Position.id_only new_id) o
+ Toplevel.imperative (fn () => edit_document old_id new_id edits)));
end;
--- a/src/Pure/Isar/isar_document.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala Thu Aug 05 14:35:35 2010 +0200
@@ -9,13 +9,6 @@
object Isar_Document
{
- /* unique identifiers */
-
- type State_ID = String
- type Command_ID = String
- type Document_ID = String
-
-
/* reports */
object Assign {
@@ -27,7 +20,7 @@
}
object Edit {
- def unapply(msg: XML.Tree): Option[(Command_ID, State_ID)] =
+ def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
msg match {
case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
Some(cmd_id, state_id)
@@ -44,7 +37,7 @@
/* commands */
- def define_command(id: Command_ID, text: String) {
+ def define_command(id: Document.Command_ID, text: String) {
output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
Isabelle_Syntax.encode_string(text))
}
@@ -52,36 +45,41 @@
/* documents */
- def begin_document(id: Document_ID, path: String) {
- output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " +
- Isabelle_Syntax.encode_string(path))
- }
-
- def end_document(id: Document_ID) {
- output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id))
- }
-
- def edit_document(old_id: Document_ID, new_id: Document_ID,
- edits: List[(Command_ID, Option[Command_ID])])
+ def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ edits: List[Document.Edit[Document.Command_ID]])
{
- def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
+ def append_edit(
+ edit: (Option[Document.Command_ID], Option[Document.Command_ID]), result: StringBuilder)
{
- edit match {
- case (id, None) => Isabelle_Syntax.append_string(id, result)
- case (id, Some(id2)) =>
- Isabelle_Syntax.append_string(id, result)
+ Isabelle_Syntax.append_string(edit._1 getOrElse Document.NO_ID, result)
+ edit._2 match {
+ case None =>
+ case Some(id2) =>
result.append(" ")
Isabelle_Syntax.append_string(id2, result)
}
}
+ def append_node_edit(
+ edit: (String, Option[List[(Option[Document.Command_ID], Option[Document.Command_ID])]]),
+ result: StringBuilder)
+ {
+ Isabelle_Syntax.append_string(edit._1, result)
+ edit._2 match {
+ case None =>
+ case Some(eds) =>
+ result.append(" ")
+ Isabelle_Syntax.append_list(append_edit, eds, result)
+ }
+ }
+
val buf = new StringBuilder(40)
buf.append("Isar.edit_document ")
Isabelle_Syntax.append_string(old_id, buf)
buf.append(" ")
Isabelle_Syntax.append_string(new_id, buf)
buf.append(" ")
- Isabelle_Syntax.append_list(append_edit, edits, buf)
+ Isabelle_Syntax.append_list(append_node_edit, edits, buf)
output_sync(buf.toString)
}
}
--- a/src/Pure/PIDE/change.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Pure/PIDE/change.scala Thu Aug 05 14:35:35 2010 +0200
@@ -8,11 +8,16 @@
package isabelle
+object Change
+{
+ val init = new Change(Document.NO_ID, None, Nil, Future.value(Nil, Document.init))
+}
+
class Change(
- val id: Isar_Document.Document_ID,
+ val id: Document.Version_ID,
val parent: Option[Change],
- val edits: List[Text_Edit],
- val result: Future[(List[Document.Edit], Document)])
+ val edits: List[Document.Node.Text_Edit],
+ val result: Future[(List[Document.Edit[Command]], Document)])
{
def ancestors: Iterator[Change] = new Iterator[Change]
{
@@ -28,10 +33,10 @@
def join_document: Document = result.join._2
def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
- def edit(session: Session, edits: List[Text_Edit]): Change =
+ def edit(session: Session, edits: List[Document.Node.Text_Edit]): Change =
{
val new_id = session.create_id()
- val result: Future[(List[Document.Edit], Document)] =
+ val result: Future[(List[Document.Edit[Command]], Document)] =
Future.fork {
val old_doc = join_document
old_doc.await_assignment
--- a/src/Pure/PIDE/command.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu Aug 05 14:35:35 2010 +0200
@@ -35,7 +35,7 @@
}
class Command(
- val id: Isar_Document.Command_ID,
+ val id: Document.Command_ID,
val span: Thy_Syntax.Span,
val static_parent: Option[Command] = None)
extends Session.Entity
@@ -91,7 +91,7 @@
accumulator ! Consume(message, forward)
}
- def assign_state(state_id: Isar_Document.State_ID): Command =
+ def assign_state(state_id: Document.State_ID): Command =
{
val cmd = new Command(state_id, span, Some(this))
accumulator !? Assign
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document.ML Thu Aug 05 14:35:35 2010 +0200
@@ -0,0 +1,36 @@
+(* Title: Pure/PIDE/document.ML
+ Author: Makarius
+
+Document as collection of named nodes, each consisting of an editable
+list of commands.
+*)
+
+signature DOCUMENT =
+sig
+ type state_id = string
+ type command_id = string
+ type version_id = string
+ val no_id: string
+ type edit = string * ((command_id * command_id option) list) option
+end;
+
+structure Document: DOCUMENT =
+struct
+
+(* unique identifiers *)
+
+type state_id = string;
+type command_id = string;
+type version_id = string;
+
+val no_id = "";
+
+
+(* edits *)
+
+type edit =
+ string * (*node name*)
+ ((command_id * command_id option) list) option; (*NONE: remove, SOME: insert/remove commands*)
+
+end;
+
--- a/src/Pure/PIDE/document.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Pure/PIDE/document.scala Thu Aug 05 14:35:35 2010 +0200
@@ -1,17 +1,37 @@
/* Title: Pure/PIDE/document.scala
Author: Makarius
-Document as editable list of commands.
+Document as collection of named nodes, each consisting of an editable
+list of commands.
*/
package isabelle
+import scala.collection.mutable
import scala.annotation.tailrec
object Document
{
+ /* unique identifiers */
+
+ type State_ID = String
+ type Command_ID = String
+ type Version_ID = String
+
+ val NO_ID = ""
+
+
+ /* nodes */
+
+ object Node { type Text_Edit = (String, List[isabelle.Text_Edit]) } // FIXME None: remove
+
+ type Edit[C] =
+ (String, // node name
+ Option[List[(Option[C], Option[C])]]) // None: remove, Some: insert/remove commands
+
+
/* command start positions */
def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
@@ -25,11 +45,11 @@
}
- /* empty document */
+ /* initial document */
- def empty(id: Isar_Document.Document_ID): Document =
+ val init: Document =
{
- val doc = new Document(id, Linear_Set(), Map())
+ val doc = new Document(NO_ID, Map().withDefaultValue(Linear_Set()), Map())
doc.assign_states(Nil)
doc
}
@@ -38,10 +58,8 @@
/** document edits **/
- type Edit = (Option[Command], Option[Command])
-
- def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
- edits: List[Text_Edit]): (List[Edit], Document) =
+ def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
+ edits: List[Node.Text_Edit]): (List[Edit[Command]], Document) =
{
require(old_doc.assignment.is_finished)
@@ -56,7 +74,8 @@
/* phase 1: edit individual command source */
- def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
+ @tailrec def edit_text(eds: List[Text_Edit],
+ commands: Linear_Set[Command]): Linear_Set[Command] =
{
eds match {
case e :: es =>
@@ -120,51 +139,64 @@
/* phase 3: resulting document edits */
- val commands0 = old_doc.commands
- val commands1 = edit_text(edits, commands0)
- val commands2 = parse_spans(commands1)
+ {
+ val doc_edits = new mutable.ListBuffer[Edit[Command]]
+ var nodes = old_doc.nodes
+ var former_states = old_doc.assignment.join
- val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
- val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
+ for ((name, text_edits) <- edits) {
+ val commands0 = nodes(name)
+ val commands1 = edit_text(text_edits, commands0)
+ val commands2 = parse_spans(commands1)
- val doc_edits =
- removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
- inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
+ val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
+ val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
+
+ val cmd_edits =
+ removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
+ inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
- val former_states = old_doc.assignment.join -- removed_commands
-
- (doc_edits, new Document(new_id, commands2, former_states))
+ doc_edits += (name -> Some(cmd_edits))
+ nodes += (name -> commands2)
+ former_states --= removed_commands
+ }
+ (doc_edits.toList, new Document(new_id, nodes, former_states))
+ }
}
}
class Document(
- val id: Isar_Document.Document_ID,
- val commands: Linear_Set[Command],
- former_states: Map[Command, Command])
+ val id: Document.Version_ID,
+ val nodes: Map[String, Linear_Set[Command]],
+ former_states: Map[Command, Command]) // FIXME !?
{
/* command ranges */
- def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands.iterator)
+ def commands(name: String): Linear_Set[Command] = nodes.get(name) getOrElse Linear_Set()
- def command_start(cmd: Command): Option[Int] =
- command_starts.find(_._1 == cmd).map(_._2)
+ def command_starts(name: String): Iterator[(Command, Int)] =
+ Document.command_starts(commands(name).iterator)
+
+ def command_start(name: String, cmd: Command): Option[Int] =
+ command_starts(name).find(_._1 == cmd).map(_._2)
- def command_range(i: Int): Iterator[(Command, Int)] =
- command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
+ def command_range(name: String, i: Int): Iterator[(Command, Int)] =
+ command_starts(name) dropWhile { case (cmd, start) => start + cmd.length <= i }
- def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
- command_range(i) takeWhile { case (_, start) => start < j }
+ def command_range(name: String, i: Int, j: Int): Iterator[(Command, Int)] =
+ command_range(name, i) takeWhile { case (_, start) => start < j }
- def command_at(i: Int): Option[(Command, Int)] =
+ def command_at(name: String, i: Int): Option[(Command, Int)] =
{
- val range = command_range(i)
+ val range = command_range(name, i)
if (range.hasNext) Some(range.next) else None
}
- def proper_command_at(i: Int): Option[Command] =
- command_at(i) match {
- case Some((command, _)) => commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
+ def proper_command_at(name: String, i: Int): Option[Command] =
+ command_at(name, i) match {
+ case Some((command, _)) =>
+ commands(name).reverse_iterator(command).find(cmd => !cmd.is_ignored)
case None => None
}
--- a/src/Pure/ROOT.ML Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Pure/ROOT.ML Thu Aug 05 14:35:35 2010 +0200
@@ -234,6 +234,7 @@
use "Thy/term_style.ML";
use "Thy/thy_output.ML";
use "Thy/thy_syntax.ML";
+use "PIDE/document.ML";
use "old_goals.ML";
use "Isar/outer_syntax.ML";
use "Thy/thy_info.ML";
--- a/src/Pure/System/session.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Pure/System/session.scala Thu Aug 05 14:35:35 2010 +0200
@@ -76,7 +76,6 @@
private case class Start(timeout: Int, args: List[String])
private case object Stop
- private case class Begin_Document(path: String)
private lazy val session_actor = actor {
@@ -84,8 +83,9 @@
def register(entity: Session.Entity) { entities += (entity.id -> entity) }
- var documents = Map[Isar_Document.Document_ID, Document]()
+ var documents = Map[Document.Version_ID, Document]()
def register_document(doc: Document) { documents += (doc.id -> doc) }
+ register_document(Document.init)
/* document changes */
@@ -94,22 +94,31 @@
{
require(change.parent.isDefined)
- val (changes, doc) = change.result.join
- val id_changes = changes map {
- case (c1, c2) =>
- (c1.map(_.id).getOrElse(""),
- c2 match {
- case None => None
- case Some(command) =>
- if (!lookup_command(command.id).isDefined) {
- register(command)
- prover.define_command(command.id, system.symbols.encode(command.source))
- }
- Some(command.id)
- })
- }
+ val (node_edits, doc) = change.result.join
+ val id_edits =
+ node_edits map {
+ case (name, None) => (name, None)
+ case (name, Some(cmd_edits)) =>
+ val chs =
+ cmd_edits map {
+ case (c1, c2) =>
+ val id1 = c1.map(_.id)
+ val id2 =
+ c2 match {
+ case None => None
+ case Some(command) =>
+ if (!lookup_command(command.id).isDefined) {
+ register(command)
+ prover.define_command(command.id, system.symbols.encode(command.source))
+ }
+ Some(command.id)
+ }
+ (id1, id2)
+ }
+ (name -> Some(chs))
+ }
register_document(doc)
- prover.edit_document(change.parent.get.id, doc.id, id_changes)
+ prover.edit_document(change.parent.get.id, doc.id, id_edits)
}
@@ -229,13 +238,6 @@
prover = null
}
- case Begin_Document(path: String) if prover != null =>
- val id = create_id()
- val doc = Document.empty(id)
- register_document(doc)
- prover.begin_document(id, path)
- reply(doc)
-
case change: Change if prover != null =>
handle_change(change)
@@ -304,7 +306,4 @@
def stop() { session_actor ! Stop }
def input(change: Change) { session_actor ! change }
-
- def begin_document(path: String): Document =
- (session_actor !? Begin_Document(path)).asInstanceOf[Document]
}
--- a/src/Tools/jEdit/src/jedit/document_model.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Thu Aug 05 14:35:35 2010 +0200
@@ -71,10 +71,10 @@
/* history */
- private val document_0 = session.begin_document(buffer.getName)
+ // FIXME proper error handling
+ val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2
- @volatile private var history = // owned by Swing thread
- new Change(document_0.id, None, Nil, Future.value(Nil, document_0))
+ @volatile private var history = Change.init // owned by Swing thread
def current_change(): Change = history
def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
@@ -86,7 +86,8 @@
{
Swing_Thread.assert()
(edits_buffer.toList /:
- current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits)
+ current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) =>
+ (for ((name, eds) <- change.edits if name == thy_name) yield eds).flatten ::: edits)
}
def from_current(doc: Document, offset: Int): Int =
@@ -102,7 +103,7 @@
private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
if (!edits_buffer.isEmpty) {
- val new_change = current_change().edit(session, edits_buffer.toList)
+ val new_change = current_change().edit(session, List((thy_name, edits_buffer.toList)))
edits_buffer.clear
history = new_change
new_change.result.map(_ => session.input(new_change))
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Aug 05 14:35:35 2010 +0200
@@ -106,7 +106,7 @@
Swing_Thread.now {
// FIXME cover doc states as well!!?
val document = model.recent_document()
- if (changed.exists(document.commands.contains))
+ if (changed.exists(document.commands(model.thy_name).contains))
full_repaint(document, changed)
}
@@ -122,7 +122,7 @@
val buffer = model.buffer
var visible_change = false
- for ((command, start) <- document.command_starts) {
+ for ((command, start) <- document.command_starts(model.thy_name)) {
if (changed(command)) {
val stop = start + command.length
val line1 = buffer.getLineOfOffset(model.to_current(document, start))
@@ -154,11 +154,12 @@
val command_range: Iterable[(Command, Int)] =
{
- val range = document.command_range(from_current(start(0)))
+ val range = document.command_range(model.thy_name, from_current(start(0)))
if (range.hasNext) {
val (cmd0, start0) = range.next
new Iterable[(Command, Int)] {
- def iterator = Document.command_starts(document.commands.iterator(cmd0), start0)
+ def iterator =
+ Document.command_starts(document.commands(model.thy_name).iterator(cmd0), start0)
}
}
else Iterable.empty
@@ -197,7 +198,7 @@
{
val document = model.recent_document()
val offset = model.from_current(document, text_area.xyToOffset(x, y))
- document.command_at(offset) match {
+ document.command_at(model.thy_name, offset) match {
case Some((command, command_start)) =>
document.current_state(command).type_at(offset - command_start) match {
case Some(text) => Isabelle.tooltip(text)
@@ -212,7 +213,7 @@
/* caret handling */
def selected_command(): Option[Command] =
- model.recent_document().proper_command_at(text_area.getCaretPosition)
+ model.recent_document().proper_command_at(model.thy_name, text_area.getCaretPosition)
private val caret_listener = new CaretListener {
private val delay = Swing_Thread.delay_last(session.input_delay) {
@@ -266,7 +267,7 @@
def to_current(pos: Int) = model.to_current(document, pos)
val saved_color = gfx.getColor // FIXME needed!?
try {
- for ((command, start) <- document.command_starts if !command.is_ignored) {
+ for ((command, start) <- document.command_starts(model.thy_name) if !command.is_ignored) {
val line1 = buffer.getLineOfOffset(to_current(start))
val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
val y = line_to_y(line1)
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Thu Aug 05 14:35:35 2010 +0200
@@ -44,7 +44,7 @@
case Some(model) =>
val document = model.recent_document()
val offset = model.from_current(document, original_offset)
- document.command_at(offset) match {
+ document.command_at(model.thy_name, offset) match {
case Some((command, command_start)) =>
document.current_state(command).ref_at(offset - command_start) match {
case Some(ref) =>
@@ -57,7 +57,7 @@
case Command.RefInfo(_, _, Some(id), Some(offset)) =>
Isabelle.session.lookup_entity(id) match {
case Some(ref_cmd: Command) =>
- document.command_start(ref_cmd) match {
+ document.command_start(model.thy_name, ref_cmd) match {
case Some(ref_cmd_start) =>
new Internal_Hyperlink(begin, end, line,
model.to_current(document, ref_cmd_start + offset - 1))
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Thu Aug 05 14:35:35 2010 +0200
@@ -97,7 +97,7 @@
val root = data.root
val document = model.recent_document()
for {
- (command, command_start) <- document.command_range(0)
+ (command, command_start) <- document.command_range(model.thy_name, 0)
if command.is_command && !stopped
}
{
@@ -129,7 +129,7 @@
val root = data.root
val document = model.recent_document()
- for ((command, command_start) <- document.command_range(0) if !stopped) {
+ for ((command, command_start) <- document.command_range(model.thy_name, 0) if !stopped) {
root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
{
val content = command.source(node.start, node.stop).replace('\n', ' ')
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu Aug 05 13:41:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Thu Aug 05 14:35:35 2010 +0200
@@ -166,7 +166,7 @@
var next_x = start
for {
- (command, command_start) <- document.command_range(from(start), from(stop))
+ (command, command_start) <- document.command_range(model.thy_name, from(start), from(stop))
markup <- document.current_state(command).highlight.flatten
val abs_start = to(command_start + markup.start)
val abs_stop = to(command_start + markup.stop)