# HG changeset patch # User wenzelm # Date 1281785046 -7200 # Node ID 001f2f44984ccd5271726710c52f03ff7cc07cde # Parent 8e4058f4848c309bbae2cb08d6b05c27704154cf# Parent 7eb0f6991e2582e936b73e7fc80d5d1716a806ff merged diff -r 8e4058f4848c -r 001f2f44984c src/Pure/General/linear_set.scala --- a/src/Pure/General/linear_set.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/General/linear_set.scala Sat Aug 14 13:24:06 2010 +0200 @@ -48,6 +48,12 @@ def next(elem: A): Option[A] = rep.nexts.get(elem) def prev(elem: A): Option[A] = rep.prevs.get(elem) + def get_after(hook: Option[A]): Option[A] = + hook match { + case None => rep.start + case Some(elem) => next(elem) + } + def insert_after(hook: Option[A], elem: A): Linear_Set[A] = if (contains(elem)) throw new Linear_Set.Duplicate(elem.toString) else diff -r 8e4058f4848c -r 001f2f44984c src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/General/markup.scala Sat Aug 14 13:24:06 2010 +0200 @@ -14,6 +14,20 @@ def get_string(name: String, props: List[(String, String)]): Option[String] = props.find(p => p._1 == name).map(_._2) + + def parse_long(s: String): Option[Long] = + try { Some(java.lang.Long.parseLong(s)) } + catch { case _: NumberFormatException => None } + + def get_long(name: String, props: List[(String, String)]): Option[Long] = + { + get_string(name, props) match { + case None => None + case Some(value) => parse_long(value) + } + } + + def parse_int(s: String): Option[Int] = try { Some(Integer.parseInt(s)) } catch { case _: NumberFormatException => None } diff -r 8e4058f4848c -r 001f2f44984c src/Pure/General/position.scala --- a/src/Pure/General/position.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/General/position.scala Sat Aug 14 13:24:06 2010 +0200 @@ -18,7 +18,7 @@ def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos) def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos) def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos) - def get_id(pos: T): Option[String] = Markup.get_string(Markup.ID, pos) + def get_id(pos: T): Option[Long] = Markup.get_long(Markup.ID, pos) def get_range(pos: T): Option[(Int, Int)] = (get_offset(pos), get_end_offset(pos)) match { @@ -27,6 +27,6 @@ case (None, _) => None } - object Id { def unapply(pos: T): Option[String] = get_id(pos) } + object Id { def unapply(pos: T): Option[Long] = get_id(pos) } object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) } } diff -r 8e4058f4848c -r 001f2f44984c src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/General/scan.scala Sat Aug 14 13:24:06 2010 +0200 @@ -285,8 +285,8 @@ val junk = many1(sym => !(symbols.is_blank(sym))) val bad_delimiter = - ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.BAD_INPUT, x + y) } - val bad = junk ^^ (x => Token(Token.Kind.BAD_INPUT, x)) + ("\"" | "`" | "{*" | "(*") ~ junk ^^ { case x ~ y => Token(Token.Kind.UNPARSED, x + y) } + val bad = junk ^^ (x => Token(Token.Kind.UNPARSED, x)) /* tokens */ diff -r 8e4058f4848c -r 001f2f44984c src/Pure/General/xml_data.scala --- a/src/Pure/General/xml_data.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/General/xml_data.scala Sat Aug 14 13:24:06 2010 +0200 @@ -15,6 +15,13 @@ class XML_Atom(s: String) extends Exception(s) + private def make_long_atom(i: Long): String = i.toString + + private def dest_long_atom(s: String): Long = + try { java.lang.Long.parseLong(s) } + catch { case e: NumberFormatException => throw new XML_Atom(s) } + + private def make_int_atom(i: Int): String = i.toString private def dest_int_atom(s: String): Int = @@ -71,6 +78,9 @@ } + def make_long(i: Long): XML.Body = make_string(make_long_atom(i)) + def dest_long(ts: XML.Body): Long = dest_long_atom(dest_string(ts)) + def make_int(i: Int): XML.Body = make_string(make_int_atom(i)) def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts)) diff -r 8e4058f4848c -r 001f2f44984c src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/Isar/isar_document.ML Sat Aug 14 13:24:06 2010 +0200 @@ -20,38 +20,37 @@ Synchronized.change_result id_count (fn i => let val i' = i + 1 - in ("i" ^ string_of_int i', i') end); + in (i', i') end); end; -fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id); -fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ quote id); - +fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document.print_id id); +fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id); (** 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*) +datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option}; +type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*) type document = node Graph.T; (*development graph via static imports*) (* command entries *) -fun make_entry next state = Entry {next = next, state = state}; +fun make_entry next exec = Entry {next = next, exec = exec}; fun the_entry (node: node) (id: Document.command_id) = - (case Symtab.lookup node id of + (case Inttab.lookup node id of NONE => err_undef "command entry" id | SOME (Entry entry) => entry); -fun put_entry (id: Document.command_id, entry: entry) = Symtab.update (id, entry); +fun put_entry (id: Document.command_id, entry: entry) = Inttab.update (id, entry); -fun put_entry_state (id: Document.command_id) state (node: node) = +fun put_entry_exec (id: Document.command_id) exec (node: node) = let val {next, ...} = the_entry node id - in put_entry (id, make_entry next state) node end; + in put_entry (id, make_entry next exec) 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); +fun reset_entry_exec id = put_entry_exec id NONE; +fun set_entry_exec (id, exec_id) = put_entry_exec id (SOME exec_id); (* iterate entries *) @@ -62,7 +61,7 @@ | apply (SOME id) x = let val entry = the_entry node id in apply (#next entry) (f (id, entry) x) end; - in if Symtab.defined node id0 then apply (SOME id0) else I end; + in if Inttab.defined node id0 then apply (SOME id0) else I end; fun first_entry P (node: node) = let @@ -76,27 +75,27 @@ (* modify entries *) fun insert_after (id: Document.command_id) (id2: Document.command_id) (node: node) = - let val {next, state} = the_entry node id in + let val {next, exec} = the_entry node id in node - |> put_entry (id, make_entry (SOME id2) state) + |> put_entry (id, make_entry (SOME id2) exec) |> put_entry (id2, make_entry next NONE) end; fun delete_after (id: Document.command_id) (node: node) = - let val {next, state} = the_entry node id in + let val {next, exec} = the_entry node id in (case next of - NONE => error ("No next entry to delete: " ^ quote id) + NONE => error ("No next entry to delete: " ^ Document.print_id id) | SOME id2 => 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)) + NONE => put_entry (id, make_entry NONE exec) + | SOME id3 => put_entry (id, make_entry (SOME id3) exec) #> reset_entry_exec id3)) end; (* node operations *) -val empty_node: node = Symtab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))]; +val empty_node: node = Inttab.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; @@ -113,24 +112,24 @@ (** global configuration **) -(* states *) +(* command executions *) local -val global_states = - Unsynchronized.ref (Symtab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]); +val global_execs = + Unsynchronized.ref (Inttab.make [(Document.no_id, Lazy.value (SOME Toplevel.toplevel))]); in -fun define_state (id: Document.state_id) state = +fun define_exec (id: Document.exec_id) exec = NAMED_CRITICAL "Isar" (fn () => - Unsynchronized.change global_states (Symtab.update_new (id, state)) - handle Symtab.DUP dup => err_dup "state" dup); + Unsynchronized.change global_execs (Inttab.update_new (id, exec)) + handle Inttab.DUP dup => err_dup "exec" dup); -fun the_state (id: Document.state_id) = - (case Symtab.lookup (! global_states) id of - NONE => err_undef "state" id - | SOME state => state); +fun the_exec (id: Document.exec_id) = + (case Inttab.lookup (! global_execs) id of + NONE => err_undef "exec" id + | SOME exec => exec); end; @@ -139,23 +138,24 @@ local -val global_commands = Unsynchronized.ref (Symtab.make [(Document.no_id, Toplevel.empty)]); +val global_commands = Unsynchronized.ref (Inttab.make [(Document.no_id, Toplevel.empty)]); in fun define_command (id: Document.command_id) text = let + val id_string = Document.print_id id; val tr = - Position.setmp_thread_data (Position.id_only id) (fn () => - Outer_Syntax.prepare_command (Position.id id) text) (); + Position.setmp_thread_data (Position.id_only id_string) (fn () => + Outer_Syntax.prepare_command (Position.id id_string) text) (); in 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) + Unsynchronized.change global_commands (Inttab.update_new (id, Toplevel.put_id id_string tr)) + handle Inttab.DUP dup => err_dup "command" dup) end; fun the_command (id: Document.command_id) = - (case Symtab.lookup (! global_commands) id of + (case Inttab.lookup (! global_commands) id of NONE => err_undef "command" id | SOME tr => tr); @@ -166,17 +166,17 @@ local -val global_documents = Unsynchronized.ref (Symtab.make [(Document.no_id, Graph.empty: document)]); +val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]); in 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); + Unsynchronized.change global_documents (Inttab.update_new (id, document)) + handle Inttab.DUP dup => err_dup "document" dup); fun the_document (id: Document.version_id) = - (case Symtab.lookup (! global_documents) id of + (case Inttab.lookup (! global_documents) id of NONE => err_undef "document" id | SOME document => document); @@ -192,8 +192,8 @@ 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)); +fun force_exec NONE = () + | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec exec_id)); in @@ -209,7 +209,7 @@ let val _ = await_cancellation (); val exec = - fold_entries Document.no_id (fn (_, {state, ...}) => fn () => force_state state) + fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec) (the_node document name); in exec () end)); in execution := new_execution end); @@ -221,57 +221,58 @@ local -fun is_changed node' (id, {next = _, state}) = +fun is_changed node' (id, {next = _, exec}) = (case try (the_entry node') id of NONE => true - | SOME {next = _, state = state'} => state' <> state); + | SOME {next = _, exec = exec'} => exec' <> exec); -fun new_state name (id: Document.command_id) (state_id, updates) = +fun new_exec name (id: Document.command_id) (exec_id, updates) = let - val state = the_state state_id; - val state_id' = create_id (); - val tr = Toplevel.put_id state_id' (the_command id); - val state' = + val exec = the_exec exec_id; + val exec_id' = create_id (); + val tr = Toplevel.put_id (Document.print_id exec_id') (the_command id); + val exec' = Lazy.lazy (fn () => - (case Lazy.force state of + (case Lazy.force exec of NONE => NONE | SOME st => Toplevel.run_command name tr st)); - val _ = define_state state_id' state'; - in (state_id', (id, state_id') :: updates) end; + val _ = define_exec exec_id' exec'; + in (exec_id', (id, exec_id') :: updates) end; -fun updates_status updates = - implode (map (fn (id, state_id) => Markup.markup (Markup.edit id state_id) "") updates) +fun updates_status new_id updates = + implode (map (fn (id, exec_id) => + Markup.markup (Markup.edit (Document.print_id id) (Document.print_id exec_id)) "") updates) |> Markup.markup Markup.assign - |> Output.status; + |> Position.setmp_thread_data (Position.id_only (Document.print_id new_id)) Output.status; + (*FIXME avoid setmp -- direct message argument*) in fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits = - Position.setmp_thread_data (Position.id_only new_id) (fn () => - NAMED_CRITICAL "Isar" (fn () => - let - val old_document = the_document old_id; - val new_document = fold edit_nodes edits old_document; + NAMED_CRITICAL "Isar" (fn () => + let + val old_document = the_document old_id; + val new_document = fold edit_nodes edits old_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 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); + 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_exec_id = the (#exec (the_entry node (the prev))); + val (_, updates) = fold_entries id (new_exec name o #1) node (prev_exec_id, []); + val node' = fold set_entry_exec 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)); + (* 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 _ = updates_status (flat updatess); - val _ = execute new_document'; - in () end)) (); + val _ = define_document new_id new_document'; + val _ = updates_status new_id (flat updatess); + val _ = execute new_document'; + in () end); end; @@ -281,16 +282,16 @@ val _ = Isabelle_Process.add_command "Isar_Document.define_command" - (fn [id, text] => define_command id text); + (fn [id, text] => define_command (Document.parse_id id) text); val _ = Isabelle_Process.add_command "Isar_Document.edit_document" (fn [old_id, new_id, edits] => - edit_document old_id new_id + edit_document (Document.parse_id old_id) (Document.parse_id new_id) (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string (XML_Data.dest_option (XML_Data.dest_list - (XML_Data.dest_pair XML_Data.dest_string - (XML_Data.dest_option XML_Data.dest_string))))) (YXML.parse_body edits))); + (XML_Data.dest_pair XML_Data.dest_int + (XML_Data.dest_option XML_Data.dest_int))))) (YXML.parse_body edits))); end; diff -r 8e4058f4848c -r 001f2f44984c src/Pure/Isar/isar_document.scala --- a/src/Pure/Isar/isar_document.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/Isar/isar_document.scala Sat Aug 14 13:24:06 2010 +0200 @@ -12,18 +12,24 @@ /* protocol messages */ object Assign { - def unapply(msg: XML.Tree): Option[List[XML.Tree]] = + def unapply(msg: XML.Tree): Option[List[(Document.Command_ID, Document.Exec_ID)]] = msg match { - case XML.Elem(Markup.Assign, edits) => Some(edits) + case XML.Elem(Markup.Assign, edits) => + val id_edits = edits.map(Edit.unapply) + if (id_edits.forall(_.isDefined)) Some(id_edits.map(_.get)) + else None case _ => None } } object Edit { - def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] = + def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.Exec_ID)] = msg match { case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) => - Some(cmd_id, state_id) + (Markup.parse_long(cmd_id), Markup.parse_long(state_id)) match { + case (Some(i), Some(j)) => Some((i, j)) + case _ => None + } case _ => None } } @@ -38,7 +44,7 @@ /* commands */ def define_command(id: Document.Command_ID, text: String): Unit = - input("Isar_Document.define_command", id, text) + input("Isar_Document.define_command", Document.print_id(id), text) /* documents */ @@ -47,13 +53,15 @@ edits: List[Document.Edit[Document.Command_ID]]) { def make_id1(id1: Option[Document.Command_ID]): XML.Body = - XML_Data.make_string(id1 getOrElse Document.NO_ID) + XML_Data.make_long(id1 getOrElse Document.NO_ID) + val arg = XML_Data.make_list( XML_Data.make_pair(XML_Data.make_string)( XML_Data.make_option(XML_Data.make_list( - XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_string))))))(edits) + XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits) - input("Isar_Document.edit_document", old_id, new_id, YXML.string_of_body(arg)) + input("Isar_Document.edit_document", + Document.print_id(old_id), Document.print_id(new_id), YXML.string_of_body(arg)) } } diff -r 8e4058f4848c -r 001f2f44984c src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/Isar/token.scala Sat Aug 14 13:24:06 2010 +0200 @@ -27,7 +27,6 @@ val VERBATIM = Value("verbatim text") val SPACE = Value("white space") val COMMENT = Value("comment text") - val BAD_INPUT = Value("bad input") val UNPARSED = Value("unparsed input") } @@ -79,7 +78,6 @@ def is_space: Boolean = kind == Token.Kind.SPACE def is_comment: Boolean = kind == Token.Kind.COMMENT def is_ignored: Boolean = is_space || is_comment - def is_unparsed: Boolean = kind == Token.Kind.UNPARSED def content: String = if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source) diff -r 8e4058f4848c -r 001f2f44984c src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/PIDE/command.scala Sat Aug 14 13:24:06 2010 +0200 @@ -1,5 +1,4 @@ /* Title: Pure/PIDE/command.scala - Author: Johannes Hölzl, TU Munich Author: Fabian Immler, TU Munich Author: Makarius @@ -13,9 +12,6 @@ import scala.collection.mutable -case class Command_Set(set: Set[Command]) - - object Command { object Status extends Enumeration @@ -31,14 +27,128 @@ } case class TypeInfo(ty: String) case class RefInfo(file: Option[String], line: Option[Int], - command_id: Option[String], offset: Option[Int]) + command_id: Option[Document.Command_ID], offset: Option[Int]) // FIXME Command_ID vs. Exec_ID !? + + + + /** accumulated results from prover **/ + + case class State( + val command: Command, + val status: Command.Status.Value, + val forks: Int, + val reverse_results: List[XML.Tree], + val markup: Markup_Text) + { + /* content */ + + lazy val results = reverse_results.reverse + + def add_result(result: XML.Tree): State = copy(reverse_results = result :: reverse_results) + + def add_markup(node: Markup_Tree): State = copy(markup = markup + node) + + + /* markup */ + + lazy val highlight: Markup_Text = + { + markup.filter(_.info match { + case Command.HighlightInfo(_, _) => true + case _ => false + }) + } + + private lazy val types: List[Markup_Node] = + markup.filter(_.info match { + case Command.TypeInfo(_) => true + case _ => false }).flatten + + def type_at(pos: Int): Option[String] = + { + types.find(t => t.start <= pos && pos < t.stop) match { + case Some(t) => + t.info match { + case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty) + case _ => None + } + case None => None + } + } + + private lazy val refs: List[Markup_Node] = + markup.filter(_.info match { + case Command.RefInfo(_, _, _, _) => true + case _ => false }).flatten + + def ref_at(pos: Int): Option[Markup_Node] = + refs.find(t => t.start <= pos && pos < t.stop) + + + /* message dispatch */ + + def accumulate(message: XML.Tree): Command.State = + message match { + case XML.Elem(Markup(Markup.STATUS, _), elems) => + (this /: elems)((state, elem) => + elem match { + case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.copy(status = Command.Status.UNPROCESSED) + case XML.Elem(Markup(Markup.FINISHED, _), _) => state.copy(status = Command.Status.FINISHED) + case XML.Elem(Markup(Markup.FAILED, _), _) => state.copy(status = Command.Status.FAILED) + case XML.Elem(Markup(Markup.FORKED, _), _) => state.copy(forks = state.forks + 1) + case XML.Elem(Markup(Markup.JOINED, _), _) => state.copy(forks = state.forks - 1) + case _ => System.err.println("Ignored status message: " + elem); state + }) + + case XML.Elem(Markup(Markup.REPORT, _), elems) => + (this /: elems)((state, elem) => + elem match { + case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => + atts match { + case Position.Range(begin, end) => + if (kind == Markup.ML_TYPING) { + val info = Pretty.string_of(body, margin = 40) + state.add_markup( + command.markup_node(begin - 1, end - 1, Command.TypeInfo(info))) + } + else if (kind == Markup.ML_REF) { + body match { + case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) => + state.add_markup( + command.markup_node( + begin - 1, end - 1, + Command.RefInfo( + Position.get_file(props), + Position.get_line(props), + Position.get_id(props), + Position.get_offset(props)))) + case _ => state + } + } + else { + state.add_markup( + command.markup_node(begin - 1, end - 1, + Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) + } + case _ => state + } + case _ => System.err.println("Ignored report message: " + elem); state + }) + case _ => add_result(message) + } + } + + + /* unparsed dummy commands */ + + def unparsed(source: String) = + new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source))) } + class Command( val id: Document.Command_ID, - val span: Thy_Syntax.Span, - val static_parent: Option[Command] = None) // FIXME !? - extends Session.Entity + val span: List[Token]) { /* classification */ @@ -46,6 +156,8 @@ def is_ignored: Boolean = span.forall(_.is_ignored) def is_malformed: Boolean = !is_command && !is_ignored + def is_unparsed = id == Document.NO_ID + def name: String = if (is_command) span.head.content else "" override def toString = id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") @@ -60,54 +172,18 @@ lazy val symbol_index = new Symbol.Index(source) - /* accumulated messages */ - - @volatile protected var state = new State(this) - def current_state: State = state - - private case class Consume(message: XML.Tree, forward: Command => Unit) - private case object Assign - - private val accumulator = actor { - var assigned = false - loop { - react { - case Consume(message, forward) if !assigned => - val old_state = state - state = old_state.accumulate(message) - if (!(state eq old_state)) forward(static_parent getOrElse this) - - case Assign => - assigned = true // single assignment - reply(()) - - case bad => System.err.println("Command accumulator: ignoring bad message " + bad) - } - } - } - - def consume(message: XML.Tree, forward: Command => Unit) - { - accumulator ! Consume(message, forward) - } - - def assign_state(state_id: Document.State_ID): Command = - { - val cmd = new Command(state_id, span, Some(this)) - accumulator !? Assign - cmd.state = current_state - cmd - } - - /* markup */ - lazy val empty_markup = new Markup_Text(Nil, source) - def markup_node(begin: Int, end: Int, info: Any): Markup_Tree = { val start = symbol_index.decode(begin) val stop = symbol_index.decode(end) new Markup_Tree(new Markup_Node(start, stop, info), Nil) } + + + /* accumulated results */ + + def empty_state: Command.State = + Command.State(this, Command.Status.UNPROCESSED, 0, Nil, new Markup_Text(Nil, source)) } diff -r 8e4058f4848c -r 001f2f44984c src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/PIDE/document.ML Sat Aug 14 13:24:06 2010 +0200 @@ -7,10 +7,13 @@ signature DOCUMENT = sig - type state_id = string - type command_id = string - type version_id = string - val no_id: string + type id = int + type version_id = id + type command_id = id + type exec_id = id + val no_id: id + val parse_id: string -> id + val print_id: id -> string type edit = string * ((command_id * command_id option) list) option end; @@ -19,11 +22,19 @@ (* unique identifiers *) -type state_id = string; -type command_id = string; -type version_id = string; +type id = int; +type version_id = id; +type command_id = id; +type exec_id = id; + +val no_id = 0; -val no_id = ""; +fun parse_id s = + (case Int.fromString s of + SOME i => i + | NONE => raise Fail ("Bad id: " ^ quote s)); + +val print_id = signed_string_of_int; (* edits *) diff -r 8e4058f4848c -r 001f2f44984c src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/PIDE/document.scala Sat Aug 14 13:24:06 2010 +0200 @@ -9,18 +9,21 @@ import scala.collection.mutable -import scala.annotation.tailrec object Document { /* formal identifiers */ - type Version_ID = String - type Command_ID = String - type State_ID = String + type ID = Long + type Version_ID = ID + type Command_ID = ID + type Exec_ID = ID - val NO_ID = "" + val NO_ID: ID = 0 + + def parse_id(s: String): ID = java.lang.Long.parseLong(s) + def print_id(id: ID): String = id.toString @@ -74,12 +77,7 @@ /* initial document */ - val init: Document = - { - val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map()) - doc.assign_states(Nil) - doc - } + val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty)) @@ -98,161 +96,121 @@ val is_outdated: Boolean def convert(offset: Int): Int def revert(offset: Int): Int + def lookup_command(id: Command_ID): Option[Command] + def state(command: Command): Command.State } object Change { - val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init)) + val init = new Change(Future.value(Document.init), Nil, Future.value(Nil, Document.init)) } class Change( - val id: Version_ID, - val parent: Option[Change], + val prev: Future[Document], val edits: List[Node_Text_Edit], val result: Future[(List[Edit[Command]], Document)]) { - def ancestors: Iterator[Change] = new Iterator[Change] - { - private var state: Option[Change] = Some(Change.this) - def hasNext = state.isDefined - def next = - state match { - case Some(change) => state = change.parent; change - case None => throw new NoSuchElementException("next on empty iterator") - } - } - - def join_document: Document = result.join._2 - def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished - - def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot = - { - val latest = Change.this - val stable = latest.ancestors.find(_.is_assigned) - require(stable.isDefined) - - val edits = - (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) => - (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits) - lazy val reverse_edits = edits.reverse - - new Snapshot { - val document = stable.get.join_document - val node = document.nodes(name) - val is_outdated = !(pending_edits.isEmpty && latest == stable.get) - def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i)) - def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i)) - } - } + val document: Future[Document] = result.map(_._2) + def is_finished: Boolean = prev.is_finished && document.is_finished } - /** editing **/ - - 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) - - - /* unparsed dummy commands */ + /** global state -- accumulated prover results **/ - def unparsed(source: String) = - new Command(NO_ID, List(Token(Token.Kind.UNPARSED, source))) - - def is_unparsed(command: Command) = command.id == NO_ID + object State + { + class Fail(state: State) extends Exception - - /* phase 1: edit individual command source */ + val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil) - @tailrec def edit_text(eds: List[Text_Edit], - commands: Linear_Set[Command]): Linear_Set[Command] = + class Assignment(former_assignment: Map[Command, Exec_ID]) { - eds match { - case e :: es => - Node.command_starts(commands.iterator).find { - case (cmd, cmd_start) => - e.can_edit(cmd.source, cmd_start) || - e.is_insert && e.start == cmd_start + cmd.length - } match { - case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => - val (rest, text) = e.edit(cmd.source, cmd_start) - val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd - edit_text(rest.toList ::: es, new_commands) + @volatile private var tmp_assignment = former_assignment + private val promise = Future.promise[Map[Command, Exec_ID]] + def is_finished: Boolean = promise.is_finished + def join: Map[Command, Exec_ID] = promise.join + def assign(command_execs: List[(Command, Exec_ID)]) + { + promise.fulfill(tmp_assignment ++ command_execs) + tmp_assignment = Map() + } + } + } - case Some((cmd, cmd_start)) => - edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text))) + case class State( + val documents: Map[Version_ID, Document] = Map(), + val commands: Map[Command_ID, Command.State] = Map(), + val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(), + val assignments: Map[Document, State.Assignment] = Map(), + val disposed: Set[ID] = Set()) // FIXME unused!? + { + private def fail[A]: A = throw new State.Fail(this) - case None => - require(e.is_insert && e.start == 0) - edit_text(es, commands.insert_after(None, unparsed(e.text))) - } - case Nil => commands - } + def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State = + { + val id = document.id + if (documents.isDefinedAt(id) || disposed(id)) fail + copy(documents = documents + (id -> document), + assignments = assignments + (document -> new State.Assignment(former_assignment))) + } + + def define_command(command: Command): State = + { + val id = command.id + if (commands.isDefinedAt(id) || disposed(id)) fail + copy(commands = commands + (id -> command.empty_state)) } - - /* phase 2: recover command spans */ + def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command) - @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] = - { - commands.iterator.find(is_unparsed) match { - case Some(first_unparsed) => - val first = - commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head - val last = - commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last - val range = - commands.iterator(first).takeWhile(_ != last).toList ::: List(last) - - val sources = range.flatMap(_.span.map(_.source)) - val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString)) + def the_document(id: Version_ID): Document = documents.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_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail) - val (before_edit, spans1) = - if (!spans0.isEmpty && first.is_command && first.span == spans0.head) - (Some(first), spans0.tail) - else (commands.prev(first), spans0) + def accumulate(id: ID, message: XML.Tree): (Command.State, State) = + execs.get(id) match { + case Some((st, docs)) => + val new_st = st.accumulate(message) + (new_st, copy(execs = execs + (id -> (new_st, docs)))) + case None => + commands.get(id) match { + case Some(st) => + val new_st = st.accumulate(message) + (new_st, copy(commands = commands + (id -> new_st))) + case None => fail + } + } - val (after_edit, spans2) = - if (!spans1.isEmpty && last.is_command && last.span == spans1.last) - (Some(last), spans1.take(spans1.length - 1)) - else (commands.next(last), spans1) + def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State = + { + val doc = the_document(id) + val docs = Set(doc) // FIXME unused (!?) - val inserted = spans2.map(span => new Command(session.create_id(), span)) - val new_commands = - commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) - parse_spans(new_commands) - - case None => commands - } + 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, docs)) + (st.command, exec_id) + } + the_assignment(doc).assign(assigned_execs) // FIXME explicit value instead of promise (!?) + copy(execs = new_execs) } - - /* phase 3: resulting document edits */ - - { - val doc_edits = new mutable.ListBuffer[Edit[Command]] - var nodes = old_doc.nodes - var former_states = old_doc.assignment.join - - for ((name, text_edits) <- edits) { - val commands0 = nodes(name).commands - val commands1 = edit_text(text_edits, commands0) - val commands2 = parse_spans(commands1) // FIXME somewhat slow + def is_assigned(document: Document): Boolean = + assignments.get(document) match { + case Some(assgn) => assgn.is_finished + case None => false + } - 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))) - - doc_edits += (name -> Some(cmd_edits)) - nodes += (name -> new Node(commands2)) - former_states --= removed_commands - } - (doc_edits.toList, new Document(new_id, nodes, former_states)) + def command_state(document: Document, command: Command): Command.State = + { + val assgn = the_assignment(document) + require(assgn.is_finished) + the_exec_state(assgn.join.getOrElse(command, fail)) } } } @@ -260,28 +218,5 @@ class Document( val id: Document.Version_ID, - val nodes: Map[String, Document.Node], - former_states: Map[Command, Command]) // FIXME !? -{ - /* command state assignment */ - - val assignment = Future.promise[Map[Command, Command]] - def await_assignment { assignment.join } - - @volatile private var tmp_states = former_states + val nodes: Map[String, Document.Node]) - def assign_states(new_states: List[(Command, Command)]) - { - assignment.fulfill(tmp_states ++ new_states) - tmp_states = Map() - } - - def current_state(cmd: Command): State = - { - require(assignment.is_finished) - (assignment.join).get(cmd) match { - case Some(cmd_state) => cmd_state.current_state - case None => new State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup) - } - } -} diff -r 8e4058f4848c -r 001f2f44984c src/Pure/PIDE/markup_node.scala --- a/src/Pure/PIDE/markup_node.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/PIDE/markup_node.scala Sat Aug 14 13:24:06 2010 +0200 @@ -2,7 +2,7 @@ Author: Fabian Immler, TU Munich Author: Makarius -Document markup nodes, with connection to Swing tree model. +Text markup nodes. */ package isabelle @@ -78,8 +78,7 @@ case class Markup_Text(val markup: List[Markup_Tree], val content: String) { - private lazy val root = - new Markup_Tree(new Markup_Node(0, content.length, None), markup) + private val root = new Markup_Tree(new Markup_Node(0, content.length, None), markup) // FIXME !? def + (new_tree: Markup_Tree): Markup_Text = new Markup_Text((root + new_tree).branches, content) diff -r 8e4058f4848c -r 001f2f44984c src/Pure/PIDE/state.scala --- a/src/Pure/PIDE/state.scala Fri Aug 13 16:40:47 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,125 +0,0 @@ -/* Title: Pure/PIDE/state.scala - Author: Fabian Immler, TU Munich - Author: Makarius - -Accumulated results from prover. -*/ - -package isabelle - - -class State( - val command: Command, - val status: Command.Status.Value, - val forks: Int, - val reverse_results: List[XML.Tree], - val markup_root: Markup_Text) -{ - def this(command: Command) = - this(command, Command.Status.UNPROCESSED, 0, Nil, command.empty_markup) - - - /* content */ - - private def set_status(st: Command.Status.Value): State = - new State(command, st, forks, reverse_results, markup_root) - - private def add_forks(i: Int): State = - new State(command, status, forks + i, reverse_results, markup_root) - - private def add_result(res: XML.Tree): State = - new State(command, status, forks, res :: reverse_results, markup_root) - - private def add_markup(node: Markup_Tree): State = - new State(command, status, forks, reverse_results, markup_root + node) - - lazy val results = reverse_results.reverse - - - /* markup */ - - lazy val highlight: Markup_Text = - { - markup_root.filter(_.info match { - case Command.HighlightInfo(_, _) => true - case _ => false - }) - } - - private lazy val types: List[Markup_Node] = - markup_root.filter(_.info match { - case Command.TypeInfo(_) => true - case _ => false }).flatten - - def type_at(pos: Int): Option[String] = - { - types.find(t => t.start <= pos && pos < t.stop) match { - case Some(t) => - t.info match { - case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + " : " + ty) - case _ => None - } - case None => None - } - } - - private lazy val refs: List[Markup_Node] = - markup_root.filter(_.info match { - case Command.RefInfo(_, _, _, _) => true - case _ => false }).flatten - - def ref_at(pos: Int): Option[Markup_Node] = - refs.find(t => t.start <= pos && pos < t.stop) - - - /* message dispatch */ - - def accumulate(message: XML.Tree): State = - message match { - case XML.Elem(Markup(Markup.STATUS, _), elems) => - (this /: elems)((state, elem) => - elem match { - case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED) - case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED) - case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED) - case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1) - case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1) - case _ => System.err.println("Ignored status message: " + elem); state - }) - - case XML.Elem(Markup(Markup.REPORT, _), elems) => - (this /: elems)((state, elem) => - elem match { - case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) => - atts match { - case Position.Range(begin, end) => - if (kind == Markup.ML_TYPING) { - val info = Pretty.string_of(body, margin = 40) - state.add_markup( - command.markup_node(begin - 1, end - 1, Command.TypeInfo(info))) - } - else if (kind == Markup.ML_REF) { - body match { - case List(XML.Elem(Markup(Markup.ML_DEF, atts), _)) => - state.add_markup(command.markup_node( - begin - 1, end - 1, - Command.RefInfo( - Position.get_file(atts), - Position.get_line(atts), - Position.get_id(atts), - Position.get_offset(atts)))) - case _ => state - } - } - else { - state.add_markup( - command.markup_node(begin - 1, end - 1, - Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts)))) - } - case _ => state - } - case _ => System.err.println("Ignored report message: " + elem); state - }) - case _ => add_result(message) - } -} diff -r 8e4058f4848c -r 001f2f44984c src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/System/isabelle_process.scala Sat Aug 14 13:24:06 2010 +0200 @@ -373,8 +373,11 @@ def input_raw(text: String): Unit = standard_input ! Input_Text(text) + def input_bytes(name: String, args: Array[Byte]*): Unit = + command_input ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList) + def input(name: String, args: String*): Unit = - command_input ! Input_Chunks((name :: args.toList).map(Standard_System.string_bytes)) + input_bytes(name, args.map(Standard_System.string_bytes): _*) def close(): Unit = command_input ! Close } diff -r 8e4058f4848c -r 001f2f44984c src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/System/isabelle_system.scala Sat Aug 14 13:24:06 2010 +0200 @@ -8,8 +8,7 @@ import java.util.regex.Pattern import java.util.Locale -import java.io.{BufferedInputStream, FileInputStream, BufferedOutputStream, FileOutputStream, - OutputStream, File, IOException} +import java.io.{InputStream, FileInputStream, OutputStream, FileOutputStream, File, IOException} import java.awt.{GraphicsEnvironment, Font} import java.awt.font.TextAttribute @@ -287,39 +286,33 @@ if (rc != 0) error(result) } - def fifo_input_stream(fifo: String): BufferedInputStream = + def fifo_input_stream(fifo: String): InputStream = { - // block until peer is ready - val stream = - if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream - val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-") - proc.getOutputStream.close - proc.getErrorStream.close - proc.getInputStream - } - else new FileInputStream(fifo) - new BufferedInputStream(stream) + if (Platform.is_windows) { // Cygwin fifo as Windows/Java input stream + val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), fifo, "-") + proc.getOutputStream.close + proc.getErrorStream.close + proc.getInputStream + } + else new FileInputStream(fifo) } - def fifo_output_stream(fifo: String): BufferedOutputStream = + def fifo_output_stream(fifo: String): OutputStream = { - // block until peer is ready - val stream = - if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream - val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo) - proc.getInputStream.close - proc.getErrorStream.close - val out = proc.getOutputStream - new OutputStream { - override def close() { out.close(); proc.waitFor() } - override def flush() { out.flush() } - override def write(b: Array[Byte]) { out.write(b) } - override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) } - override def write(b: Int) { out.write(b) } - } + if (Platform.is_windows) { // Cygwin fifo as Windows/Java output stream + val proc = execute(false, expand_path("$ISABELLE_HOME/lib/scripts/raw_dump"), "-", fifo) + proc.getInputStream.close + proc.getErrorStream.close + val out = proc.getOutputStream + new OutputStream { + override def close() { out.close(); proc.waitFor() } + override def flush() { out.flush() } + override def write(b: Array[Byte]) { out.write(b) } + override def write(b: Array[Byte], off: Int, len: Int) { out.write(b, off, len) } + override def write(b: Int) { out.write(b) } } - else new FileOutputStream(fifo) - new BufferedOutputStream(stream) + } + else new FileOutputStream(fifo) } diff -r 8e4058f4848c -r 001f2f44984c src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/System/session.scala Sat Aug 14 13:24:06 2010 +0200 @@ -19,17 +19,7 @@ case object Global_Settings case object Perspective - - - /* managed entities */ - - type Entity_ID = String - - trait Entity - { - val id: Entity_ID - def consume(message: XML.Tree, forward: Command => Unit): Unit - } + case class Commands_Changed(set: Set[Command]) } @@ -52,14 +42,18 @@ val global_settings = new Event_Bus[Session.Global_Settings.type] val raw_results = new Event_Bus[Isabelle_Process.Result] val raw_output = new Event_Bus[Isabelle_Process.Result] - val commands_changed = new Event_Bus[Command_Set] + val commands_changed = new Event_Bus[Session.Commands_Changed] val perspective = new Event_Bus[Session.Perspective.type] /* unique ids */ - private var id_count: BigInt = 0 - def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count } + private var id_count: Document.ID = 0 + def create_id(): Document.ID = synchronized { + require(id_count > java.lang.Long.MIN_VALUE) + id_count -= 1 + id_count + } @@ -68,13 +62,9 @@ @volatile private var syntax = new Outer_Syntax(system.symbols) def current_syntax: Outer_Syntax = syntax - @volatile private var entities = Map[Session.Entity_ID, Session.Entity]() - def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id) - def lookup_command(id: Session.Entity_ID): Option[Command] = - lookup_entity(id) match { - case Some(cmd: Command) => Some(cmd) - case _ => None - } + @volatile private var global_state = Document.State.init + private def change_state(f: Document.State => Document.State) { global_state = f(global_state) } + def current_state(): Document.State = global_state private case class Started(timeout: Int, args: List[String]) private case object Stop @@ -83,26 +73,29 @@ var prover: Isabelle_Process with Isar_Document = null - def register(entity: Session.Entity) { entities += (entity.id -> entity) } - - var documents = Map[Document.Version_ID, Document]() - def register_document(doc: Document) { documents += (doc.id -> doc) } - register_document(Document.init) - /* document changes */ def handle_change(change: Document.Change) //{{{ { - require(change.parent.isDefined) + require(change.is_finished) + + val old_doc = change.prev.join + val (node_edits, doc) = change.result.join - val (node_edits, doc) = change.result.join + var former_assignment = current_state().the_assignment(old_doc).join + for { + (name, Some(cmd_edits)) <- node_edits + (prev, None) <- cmd_edits + removed <- old_doc.nodes(name).commands.get_after(prev) + } former_assignment -= removed + val id_edits = node_edits map { case (name, None) => (name, None) case (name, Some(cmd_edits)) => - val chs = + val ids = cmd_edits map { case (c1, c2) => val id1 = c1.map(_.id) @@ -110,18 +103,18 @@ c2 match { case None => None case Some(command) => - if (!lookup_command(command.id).isDefined) { - register(command) + if (current_state().lookup_command(command.id).isEmpty) { + change_state(_.define_command(command)) prover.define_command(command.id, system.symbols.encode(command.source)) } Some(command.id) } (id1, id2) } - (name -> Some(chs)) + (name -> Some(ids)) } - register_document(doc) - prover.edit_document(change.parent.get.id, doc.id, id_edits) + change_state(_.define_document(doc, former_assignment)) + prover.edit_document(old_doc.id, doc.id, id_edits) } //}}} @@ -138,47 +131,38 @@ { raw_results.event(result) - val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties) - val target: Option[Session.Entity] = - target_id match { - case None => None - case Some(id) => lookup_entity(id) + Position.get_id(result.properties) match { + case Some(target_id) => + try { + val (st, state) = global_state.accumulate(target_id, result.message) + global_state = state + indicate_command_change(st.command) // FIXME forward Command.State (!?) + } + catch { + case _: Document.State.Fail => + if (result.is_status) { + result.body match { + case List(Isar_Document.Assign(edits)) => + try { change_state(_.assign(target_id, edits)) } + catch { case _: Document.State.Fail => bad_result(result) } + case _ => bad_result(result) + } + } + else bad_result(result) + } + case None => + if (result.is_status) { + result.body match { + // keyword declarations // FIXME always global!? + case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) + case List(Keyword.Keyword_Decl(name)) => syntax += name + case _ => if (!result.is_ready) bad_result(result) + } + } + else if (result.kind == Markup.EXIT) prover = null + else if (result.is_raw) raw_output.event(result) + else if (!result.is_system) bad_result(result) // FIXME syslog for system messages (!?) } - if (target.isDefined) target.get.consume(result.message, indicate_command_change) - else if (result.is_status) { - // global status message - result.body match { - - // document state assignment - case List(Isar_Document.Assign(edits)) if target_id.isDefined => - documents.get(target_id.get) match { - case Some(doc) => - val states = - for { - Isar_Document.Edit(cmd_id, state_id) <- edits - cmd <- lookup_command(cmd_id) - } yield { - val st = cmd.assign_state(state_id) - register(st) - (cmd, st) - } - doc.assign_states(states) - case None => bad_result(result) - } - - // keyword declarations - case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind) - case List(Keyword.Keyword_Decl(name)) => syntax += name - - case _ => if (!result.is_ready) bad_result(result) - } - } - else if (result.kind == Markup.EXIT) - prover = null - else if (result.is_raw) - raw_output.event(result) - else if (!result.is_system) // FIXME syslog (!?) - bad_result(result) } //}}} @@ -278,7 +262,7 @@ def flush() { - if (!changed.isEmpty) commands_changed.event(Command_Set(changed)) + if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed)) changed = Set() flush_time = None } @@ -315,25 +299,55 @@ private val editor_history = new Actor { - @volatile private var history = Document.Change.init - def current_change(): Document.Change = history + @volatile private var history = List(Document.Change.init) + + def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot = + { + val state_snapshot = current_state() + val history_snapshot = history + + val found_stable = history_snapshot.find(change => + change.is_finished && state_snapshot.is_assigned(change.document.join)) + require(found_stable.isDefined) + val stable = found_stable.get + val latest = history_snapshot.head + + val edits = + (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) => + (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits) + lazy val reverse_edits = edits.reverse + + new Document.Snapshot { + val document = stable.document.join + val node = document.nodes(name) + val is_outdated = !(pending_edits.isEmpty && latest == stable) + def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i)) + def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i)) + def lookup_command(id: Document.Command_ID): Option[Command] = + state_snapshot.lookup_command(id) + def state(command: Command): Command.State = + state_snapshot.command_state(document, command) + } + } def act { loop { react { case Edit_Document(edits) => - val old_change = history - val new_id = create_id() + val history_snapshot = history + require(!history_snapshot.isEmpty) + + val prev = history_snapshot.head.document val result: isabelle.Future[(List[Document.Edit[Command]], Document)] = isabelle.Future.fork { - val old_doc = old_change.join_document - old_doc.await_assignment - Document.text_edits(Session.this, old_doc, new_id, edits) + val old_doc = prev.join + val former_assignment = current_state().the_assignment(old_doc).join // FIXME async!? + Thy_Syntax.text_edits(Session.this, old_doc, edits) } - val new_change = new Document.Change(new_id, Some(old_change), edits, result) - history = new_change - new_change.result.map(_ => session_actor ! new_change) + val new_change = new Document.Change(prev, edits, result) + history ::= new_change + new_change.document.map(_ => session_actor ! new_change) reply(()) case bad => System.err.println("editor_model: ignoring bad message " + bad) @@ -352,7 +366,8 @@ def stop() { session_actor ! Stop } - def current_change(): Document.Change = editor_history.current_change() + def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot = + editor_history.snapshot(name, pending_edits) def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) } } diff -r 8e4058f4848c -r 001f2f44984c src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Sat Aug 14 13:24:06 2010 +0200 @@ -1,22 +1,23 @@ /* Title: Pure/Thy/thy_syntax.scala Author: Makarius -Superficial theory syntax: command spans. +Superficial theory syntax: tokens and spans. */ package isabelle import scala.collection.mutable +import scala.annotation.tailrec object Thy_Syntax { - type Span = List[Token] + /** parse spans **/ - def parse_spans(toks: List[Token]): List[Span] = + def parse_spans(toks: List[Token]): List[List[Token]] = { - val result = new mutable.ListBuffer[Span] + val result = new mutable.ListBuffer[List[Token]] val span = new mutable.ListBuffer[Token] val whitespace = new mutable.ListBuffer[Token] @@ -32,4 +33,101 @@ flush(span); flush(whitespace) result.toList } + + + + /** text edits **/ + + def text_edits(session: Session, old_doc: Document, edits: List[Document.Node_Text_Edit]) + : (List[Document.Edit[Command]], Document) = + { + /* phase 1: edit individual command source */ + + @tailrec def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]) + : Linear_Set[Command] = + { + eds match { + case e :: es => + Document.Node.command_starts(commands.iterator).find { + case (cmd, cmd_start) => + e.can_edit(cmd.source, cmd_start) || + e.is_insert && e.start == cmd_start + cmd.length + } match { + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) => + val (rest, text) = e.edit(cmd.source, cmd_start) + val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd + edit_text(rest.toList ::: es, new_commands) + + case Some((cmd, cmd_start)) => + edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text))) + + case None => + require(e.is_insert && e.start == 0) + edit_text(es, commands.insert_after(None, Command.unparsed(e.text))) + } + case Nil => commands + } + } + + + /* phase 2: recover command spans */ + + @tailrec def recover_spans(commands: Linear_Set[Command]): Linear_Set[Command] = + { + commands.iterator.find(_.is_unparsed) match { + case Some(first_unparsed) => + val first = + commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head + val last = + commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last + val range = + commands.iterator(first).takeWhile(_ != last).toList ::: List(last) + + val sources = range.flatMap(_.span.map(_.source)) + val spans0 = parse_spans(session.current_syntax.scan(sources.mkString)) + + val (before_edit, spans1) = + if (!spans0.isEmpty && first.is_command && first.span == spans0.head) + (Some(first), spans0.tail) + else (commands.prev(first), spans0) + + val (after_edit, spans2) = + if (!spans1.isEmpty && last.is_command && last.span == spans1.last) + (Some(last), spans1.take(spans1.length - 1)) + else (commands.next(last), spans1) + + val inserted = spans2.map(span => new Command(session.create_id(), span)) + val new_commands = + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted) + recover_spans(new_commands) + + case None => commands + } + } + + + /* resulting document edits */ + + { + val doc_edits = new mutable.ListBuffer[Document.Edit[Command]] + var nodes = old_doc.nodes + + for ((name, text_edits) <- edits) { + val commands0 = nodes(name).commands + val commands1 = edit_text(text_edits, commands0) + val commands2 = recover_spans(commands1) // FIXME somewhat slow + + 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))) + + doc_edits += (name -> Some(cmd_edits)) + nodes += (name -> new Document.Node(commands2)) + } + (doc_edits.toList, new Document(session.create_id(), nodes)) + } + } } diff -r 8e4058f4848c -r 001f2f44984c src/Pure/build-jars --- a/src/Pure/build-jars Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Pure/build-jars Sat Aug 14 13:24:06 2010 +0200 @@ -42,7 +42,6 @@ PIDE/document.scala PIDE/event_bus.scala PIDE/markup_node.scala - PIDE/state.scala PIDE/text_edit.scala System/cygwin.scala System/download.scala diff -r 8e4058f4848c -r 001f2f44984c src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Sat Aug 14 13:24:06 2010 +0200 @@ -227,7 +227,7 @@ def snapshot(): Document.Snapshot = { Swing_Thread.require() - session.current_change().snapshot(thy_name, pending_edits.snapshot()) + session.snapshot(thy_name, pending_edits.snapshot()) } @@ -278,7 +278,7 @@ for { (command, command_start) <- snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop)) - markup <- snapshot.document.current_state(command).highlight.flatten + markup <- snapshot.state(command).highlight.flatten val abs_start = snapshot.convert(command_start + markup.start) val abs_stop = snapshot.convert(command_start + markup.stop) if (abs_stop > start) diff -r 8e4058f4848c -r 001f2f44984c src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Sat Aug 14 13:24:06 2010 +0200 @@ -26,7 +26,7 @@ { def choose_color(snapshot: Document.Snapshot, command: Command): Color = { - val state = snapshot.document.current_state(command) + val state = snapshot.state(command) if (snapshot.is_outdated) new Color(240, 240, 240) else if (state.forks > 0) new Color(255, 228, 225) else if (state.forks < 0) Color.red @@ -103,7 +103,7 @@ private val commands_changed_actor = actor { loop { react { - case Command_Set(changed) => + case Session.Commands_Changed(changed) => Swing_Thread.now { // FIXME cover doc states as well!!? val snapshot = model.snapshot() @@ -203,7 +203,7 @@ val offset = snapshot.revert(text_area.xyToOffset(x, y)) snapshot.node.command_at(offset) match { case Some((command, command_start)) => - snapshot.document.current_state(command).type_at(offset - command_start) match { + snapshot.state(command).type_at(offset - command_start) match { case Some(text) => Isabelle.tooltip(text) case None => null } diff -r 8e4058f4848c -r 001f2f44984c src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Sat Aug 14 13:24:06 2010 +0200 @@ -47,7 +47,7 @@ val offset = snapshot.revert(original_offset) snapshot.node.command_at(offset) match { case Some((command, command_start)) => - snapshot.document.current_state(command).ref_at(offset - command_start) match { + snapshot.state(command).ref_at(offset - command_start) match { case Some(ref) => val begin = snapshot.convert(command_start + ref.start) val line = buffer.getLineOfOffset(begin) @@ -56,8 +56,8 @@ case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) => new External_Hyperlink(begin, end, line, ref_file, ref_line) case Command.RefInfo(_, _, Some(id), Some(offset)) => - Isabelle.session.lookup_entity(id) match { - case Some(ref_cmd: Command) => + snapshot.lookup_command(id) match { // FIXME Command_ID vs. Exec_ID (!??) + case Some(ref_cmd) => snapshot.node.command_start(ref_cmd) match { case Some(ref_cmd_start) => new Internal_Hyperlink(begin, end, line, diff -r 8e4058f4848c -r 001f2f44984c src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sat Aug 14 13:24:06 2010 +0200 @@ -130,7 +130,7 @@ val root = data.root val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) { - root.add(snapshot.document.current_state(command).markup_root.swing_tree((node: Markup_Node) => + root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) => { val content = command.source(node.start, node.stop).replace('\n', ' ') val id = command.id @@ -139,7 +139,7 @@ override def getIcon: Icon = null override def getShortString: String = content override def getLongString: String = node.info.toString - override def getName: String = id + override def getName: String = Document.print_id(id) override def setName(name: String) = () override def setStart(start: Position) = () override def getStart: Position = command_start + node.start diff -r 8e4058f4848c -r 001f2f44984c src/Tools/jEdit/src/jedit/output_dockable.scala --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Fri Aug 13 16:40:47 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Sat Aug 14 13:24:06 2010 +0200 @@ -67,7 +67,7 @@ case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => val snapshot = doc_view.model.snapshot() val filtered_results = - snapshot.document.current_state(cmd).results filter { + snapshot.state(cmd).results filter { case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug case _ => true @@ -87,7 +87,7 @@ loop { react { case Session.Global_Settings => handle_resize() - case Command_Set(changed) => handle_update(Some(changed)) + case Session.Commands_Changed(changed) => handle_update(Some(changed)) case Session.Perspective => if (follow_caret && handle_perspective()) handle_update() case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) }