# HG changeset patch # User wenzelm # Date 1281011735 -7200 # Node ID 67fc24df3721cdf696c3d29a37436bc7027b8bc9 # Parent 3c380380beac22413691e0498b78ba8dcdeb763b 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; diff -r 3c380380beac -r 67fc24df3721 src/Pure/IsaMakefile --- 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 \ diff -r 3c380380beac -r 67fc24df3721 src/Pure/Isar/isar_document.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; diff -r 3c380380beac -r 67fc24df3721 src/Pure/Isar/isar_document.scala --- 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) } } diff -r 3c380380beac -r 67fc24df3721 src/Pure/PIDE/change.scala --- 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 diff -r 3c380380beac -r 67fc24df3721 src/Pure/PIDE/command.scala --- 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 diff -r 3c380380beac -r 67fc24df3721 src/Pure/PIDE/document.ML --- /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; + diff -r 3c380380beac -r 67fc24df3721 src/Pure/PIDE/document.scala --- 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 } diff -r 3c380380beac -r 67fc24df3721 src/Pure/ROOT.ML --- 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"; diff -r 3c380380beac -r 67fc24df3721 src/Pure/System/session.scala --- 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] } diff -r 3c380380beac -r 67fc24df3721 src/Tools/jEdit/src/jedit/document_model.scala --- 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)) diff -r 3c380380beac -r 67fc24df3721 src/Tools/jEdit/src/jedit/document_view.scala --- 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) diff -r 3c380380beac -r 67fc24df3721 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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)) diff -r 3c380380beac -r 67fc24df3721 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- 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', ' ') diff -r 3c380380beac -r 67fc24df3721 src/Tools/jEdit/src/jedit/isabelle_token_marker.scala --- 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)