# HG changeset patch # User wenzelm # Date 1322769288 -3600 # Node ID b4e7b9968e60dfefa1363b9f857edb98faf20827 # Parent ccf2cbe86d708534f98c421b3a08dcd7c8185337# Parent 87017fcbad83977a8b59e55fc227ccb45721459d merged diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Dec 01 20:52:16 2011 +0100 +++ b/src/Pure/IsaMakefile Thu Dec 01 20:54:48 2011 +0100 @@ -154,9 +154,9 @@ ML/ml_syntax.ML \ ML/ml_thms.ML \ PIDE/document.ML \ - PIDE/isabelle_document.ML \ PIDE/isabelle_markup.ML \ PIDE/markup.ML \ + PIDE/protocol.ML \ PIDE/xml.ML \ PIDE/yxml.ML \ Proof/extraction.ML \ diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Dec 01 20:52:16 2011 +0100 +++ b/src/Pure/PIDE/command.scala Thu Dec 01 20:54:48 2011 +0100 @@ -66,11 +66,11 @@ val result = XML.Elem(Markup(name, Position.purge(atts)), body) val st0 = add_result(i, result) val st1 = - if (Isabelle_Document.is_tracing(message)) st0 + if (Protocol.is_tracing(message)) st0 else - (st0 /: Isabelle_Document.message_positions(command, message))( + (st0 /: Protocol.message_positions(command, message))( (st, range) => st.add_markup(Text.Info(range, result))) - val st2 = (st1 /: Isabelle_Document.message_reports(message))(_ accumulate _) + val st2 = (st1 /: Protocol.message_reports(message))(_ accumulate _) st2 case _ => System.err.println("Ignored message without serial number: " + message); this } diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/PIDE/isabelle_document.ML --- a/src/Pure/PIDE/isabelle_document.ML Thu Dec 01 20:52:16 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,84 +0,0 @@ -(* Title: Pure/PIDE/isabelle_document.ML - Author: Makarius - -Protocol message formats for interactive Isar documents. -*) - -structure Isabelle_Document: sig end = -struct - -val _ = - Isabelle_Process.add_command "Isabelle_Document.define_command" - (fn [id, name, text] => - Document.change_state (Document.define_command (Document.parse_id id) name text)); - -val _ = - Isabelle_Process.add_command "Isabelle_Document.cancel_execution" - (fn [] => ignore (Document.cancel_execution (Document.state ()))); - -val _ = - Isabelle_Process.add_command "Isabelle_Document.update_perspective" - (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state => - let - val old_id = Document.parse_id old_id_string; - val new_id = Document.parse_id new_id_string; - val ids = YXML.parse_body ids_yxml - |> let open XML.Decode in list int end; - - val _ = Future.join_tasks (Document.cancel_execution state); - in - state - |> Document.update_perspective old_id new_id name ids - |> Document.execute new_id - end)); - -val _ = - Isabelle_Process.add_command "Isabelle_Document.update" - (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => - let - val old_id = Document.parse_id old_id_string; - val new_id = Document.parse_id new_id_string; - val edits = - YXML.parse_body edits_yxml |> - let open XML.Decode in - list (pair string - (variant - [fn ([], []) => Document.Clear, - fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), - fn ([], a) => - Document.Header - (Exn.Res - (triple (pair string string) (list string) (list (pair string bool)) a)), - fn ([a], []) => Document.Header (Exn.Exn (ERROR a)), - fn (a, []) => Document.Perspective (map int_atom a)])) - end; - - val running = Document.cancel_execution state; - val (assignment, state1) = Document.update old_id new_id edits state; - val _ = Future.join_tasks running; - val _ = - Output.raw_message Isabelle_Markup.assign_execs - ((new_id, assignment) |> - let open XML.Encode - in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end - |> YXML.string_of_body); - val state2 = Document.execute new_id state1; - in state2 end)); - -val _ = - Isabelle_Process.add_command "Isabelle_Document.remove_versions" - (fn [versions_yxml] => Document.change_state (fn state => - let - val versions = - YXML.parse_body versions_yxml |> - let open XML.Decode in list int end; - val state1 = Document.remove_versions versions state; - val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml; - in state1 end)); - -val _ = - Isabelle_Process.add_command "Isabelle_Document.invoke_scala" - (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res); - -end; - diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/PIDE/isabelle_document.scala --- a/src/Pure/PIDE/isabelle_document.scala Thu Dec 01 20:52:16 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,231 +0,0 @@ -/* Title: Pure/PIDE/isabelle_document.scala - Author: Makarius - -Protocol message formats for interactive Isar documents. -*/ - -package isabelle - - -object Isabelle_Document -{ - /* document editing */ - - object Assign - { - def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] = - try { - import XML.Decode._ - val body = YXML.parse_body(text) - Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body)) - } - catch { - case ERROR(_) => None - case _: XML.XML_Atom => None - case _: XML.XML_Body => None - } - } - - object Removed - { - def unapply(text: String): Option[List[Document.Version_ID]] = - try { - import XML.Decode._ - Some(list(long)(YXML.parse_body(text))) - } - catch { - case ERROR(_) => None - case _: XML.XML_Atom => None - case _: XML.XML_Body => None - } - } - - - /* toplevel transactions */ - - sealed abstract class Status - case object Unprocessed extends Status - case class Forked(forks: Int) extends Status - case object Finished extends Status - case object Failed extends Status - - def command_status(markup: List[Markup]): Status = - { - val forks = (0 /: markup) { - case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1 - case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1 - case (i, _) => i - } - if (forks != 0) Forked(forks) - else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed - else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished - else Unprocessed - } - - sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int) - { - def total: Int = unprocessed + running + finished + failed - } - - def node_status( - state: Document.State, version: Document.Version, node: Document.Node): Node_Status = - { - var unprocessed = 0 - var running = 0 - var finished = 0 - var failed = 0 - node.commands.foreach(command => - command_status(state.command_state(version, command).status) match { - case Unprocessed => unprocessed += 1 - case Forked(_) => running += 1 - case Finished => finished += 1 - case Failed => failed += 1 - }) - Node_Status(unprocessed, running, finished, failed) - } - - - /* result messages */ - - def clean_message(body: XML.Body): XML.Body = - body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map - { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t } - - def message_reports(msg: XML.Tree): List[XML.Elem] = - msg match { - case elem @ XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => List(elem) - case XML.Elem(_, body) => body.flatMap(message_reports) - case XML.Text(_) => Nil - } - - - /* specific messages */ - - def is_ready(msg: XML.Tree): Boolean = - msg match { - case XML.Elem(Markup(Isabelle_Markup.STATUS, _), - List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true - case _ => false - } - - def is_tracing(msg: XML.Tree): Boolean = - msg match { - case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true - case _ => false - } - - def is_warning(msg: XML.Tree): Boolean = - msg match { - case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true - case _ => false - } - - def is_error(msg: XML.Tree): Boolean = - msg match { - case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true - case _ => false - } - - def is_state(msg: XML.Tree): Boolean = - msg match { - case XML.Elem(Markup(Isabelle_Markup.WRITELN, _), - List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true - case _ => false - } - - - /* reported positions */ - - private val include_pos = - Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT, - Isabelle_Markup.POSITION) - - def message_positions(command: Command, message: XML.Elem): Set[Text.Range] = - { - def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = - tree match { - case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body) - if include_pos(name) && id == command.id => - val range = command.decode(raw_range).restrict(command.range) - body.foldLeft(if (range.is_singularity) set else set + range)(positions) - case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions) - case _ => set - } - val set = positions(Set.empty, message) - if (set.isEmpty && !is_state(message)) - set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_)) - else set - } -} - - -trait Isabelle_Document extends Isabelle_Process -{ - /* commands */ - - def define_command(command: Command): Unit = - input("Isabelle_Document.define_command", - Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source)) - - - /* document versions */ - - def cancel_execution() - { - input("Isabelle_Document.cancel_execution") - } - - def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID, - name: Document.Node.Name, perspective: Command.Perspective) - { - val ids = - { import XML.Encode._ - list(long)(perspective.commands.map(_.id)) } - - input("Isabelle_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), - name.node, YXML.string_of_body(ids)) - } - - def update(old_id: Document.Version_ID, new_id: Document.Version_ID, - edits: List[Document.Edit_Command]) - { - val edits_yxml = - { import XML.Encode._ - def id: T[Command] = (cmd => long(cmd.id)) - def encode_edit(dir: String) - : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] = - variant(List( - { case Document.Node.Clear() => (Nil, Nil) }, - { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, - { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) => - (Nil, - triple(pair(string, string), list(string), list(pair(string, bool)))( - (dir, a), b, c)) }, - { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }, - { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) - def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => - { - val (name, edit) = node_edit - val dir = Isabelle_System.posix_path(name.dir) - pair(string, encode_edit(dir))(name.node, edit) - }) - YXML.string_of_body(encode(edits)) } - input("Isabelle_Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml) - } - - def remove_versions(versions: List[Document.Version]) - { - val versions_yxml = - { import XML.Encode._ - YXML.string_of_body(list(long)(versions.map(_.id))) } - input("Isabelle_Document.remove_versions", versions_yxml) - } - - - /* method invocation service */ - - def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String) - { - input("Isabelle_Document.invoke_scala", id, tag.toString, res) - } -} diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/PIDE/protocol.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/protocol.ML Thu Dec 01 20:54:48 2011 +0100 @@ -0,0 +1,84 @@ +(* Title: Pure/PIDE/protocol.ML + Author: Makarius + +Protocol message formats for interactive proof documents. +*) + +structure Protocol: sig end = +struct + +val _ = + Isabelle_Process.add_command "Document.define_command" + (fn [id, name, text] => + Document.change_state (Document.define_command (Document.parse_id id) name text)); + +val _ = + Isabelle_Process.add_command "Document.cancel_execution" + (fn [] => ignore (Document.cancel_execution (Document.state ()))); + +val _ = + Isabelle_Process.add_command "Document.update_perspective" + (fn [old_id_string, new_id_string, name, ids_yxml] => Document.change_state (fn state => + let + val old_id = Document.parse_id old_id_string; + val new_id = Document.parse_id new_id_string; + val ids = YXML.parse_body ids_yxml + |> let open XML.Decode in list int end; + + val _ = Future.join_tasks (Document.cancel_execution state); + in + state + |> Document.update_perspective old_id new_id name ids + |> Document.execute new_id + end)); + +val _ = + Isabelle_Process.add_command "Document.update" + (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => + let + val old_id = Document.parse_id old_id_string; + val new_id = Document.parse_id new_id_string; + val edits = + YXML.parse_body edits_yxml |> + let open XML.Decode in + list (pair string + (variant + [fn ([], []) => Document.Clear, + fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), + fn ([], a) => + Document.Header + (Exn.Res + (triple (pair string string) (list string) (list (pair string bool)) a)), + fn ([a], []) => Document.Header (Exn.Exn (ERROR a)), + fn (a, []) => Document.Perspective (map int_atom a)])) + end; + + val running = Document.cancel_execution state; + val (assignment, state1) = Document.update old_id new_id edits state; + val _ = Future.join_tasks running; + val _ = + Output.raw_message Isabelle_Markup.assign_execs + ((new_id, assignment) |> + let open XML.Encode + in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end + |> YXML.string_of_body); + val state2 = Document.execute new_id state1; + in state2 end)); + +val _ = + Isabelle_Process.add_command "Document.remove_versions" + (fn [versions_yxml] => Document.change_state (fn state => + let + val versions = + YXML.parse_body versions_yxml |> + let open XML.Decode in list int end; + val state1 = Document.remove_versions versions state; + val _ = Output.raw_message Isabelle_Markup.removed_versions versions_yxml; + in state1 end)); + +val _ = + Isabelle_Process.add_command "Document.invoke_scala" + (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res); + +end; + diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/PIDE/protocol.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/protocol.scala Thu Dec 01 20:54:48 2011 +0100 @@ -0,0 +1,231 @@ +/* Title: Pure/PIDE/protocol.scala + Author: Makarius + +Protocol message formats for interactive proof documents. +*/ + +package isabelle + + +object Protocol +{ + /* document editing */ + + object Assign + { + def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] = + try { + import XML.Decode._ + val body = YXML.parse_body(text) + Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body)) + } + catch { + case ERROR(_) => None + case _: XML.XML_Atom => None + case _: XML.XML_Body => None + } + } + + object Removed + { + def unapply(text: String): Option[List[Document.Version_ID]] = + try { + import XML.Decode._ + Some(list(long)(YXML.parse_body(text))) + } + catch { + case ERROR(_) => None + case _: XML.XML_Atom => None + case _: XML.XML_Body => None + } + } + + + /* toplevel transactions */ + + sealed abstract class Status + case object Unprocessed extends Status + case class Forked(forks: Int) extends Status + case object Finished extends Status + case object Failed extends Status + + def command_status(markup: List[Markup]): Status = + { + val forks = (0 /: markup) { + case (i, Markup(Isabelle_Markup.FORKED, _)) => i + 1 + case (i, Markup(Isabelle_Markup.JOINED, _)) => i - 1 + case (i, _) => i + } + if (forks != 0) Forked(forks) + else if (markup.exists(_.name == Isabelle_Markup.FAILED)) Failed + else if (markup.exists(_.name == Isabelle_Markup.FINISHED)) Finished + else Unprocessed + } + + sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int) + { + def total: Int = unprocessed + running + finished + failed + } + + def node_status( + state: Document.State, version: Document.Version, node: Document.Node): Node_Status = + { + var unprocessed = 0 + var running = 0 + var finished = 0 + var failed = 0 + node.commands.foreach(command => + command_status(state.command_state(version, command).status) match { + case Unprocessed => unprocessed += 1 + case Forked(_) => running += 1 + case Finished => finished += 1 + case Failed => failed += 1 + }) + Node_Status(unprocessed, running, finished, failed) + } + + + /* result messages */ + + def clean_message(body: XML.Body): XML.Body = + body filter { case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false case _ => true } map + { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t } + + def message_reports(msg: XML.Tree): List[XML.Elem] = + msg match { + case elem @ XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => List(elem) + case XML.Elem(_, body) => body.flatMap(message_reports) + case XML.Text(_) => Nil + } + + + /* specific messages */ + + def is_ready(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(Isabelle_Markup.STATUS, _), + List(XML.Elem(Markup(Isabelle_Markup.READY, _), _))) => true + case _ => false + } + + def is_tracing(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true + case _ => false + } + + def is_warning(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true + case _ => false + } + + def is_error(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true + case _ => false + } + + def is_state(msg: XML.Tree): Boolean = + msg match { + case XML.Elem(Markup(Isabelle_Markup.WRITELN, _), + List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true + case _ => false + } + + + /* reported positions */ + + private val include_pos = + Set(Isabelle_Markup.BINDING, Isabelle_Markup.ENTITY, Isabelle_Markup.REPORT, + Isabelle_Markup.POSITION) + + def message_positions(command: Command, message: XML.Elem): Set[Text.Range] = + { + def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = + tree match { + case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body) + if include_pos(name) && id == command.id => + val range = command.decode(raw_range).restrict(command.range) + body.foldLeft(if (range.is_singularity) set else set + range)(positions) + case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions) + case _ => set + } + val set = positions(Set.empty, message) + if (set.isEmpty && !is_state(message)) + set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_)) + else set + } +} + + +trait Protocol extends Isabelle_Process +{ + /* commands */ + + def define_command(command: Command): Unit = + input("Document.define_command", + Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source)) + + + /* document versions */ + + def cancel_execution() + { + input("Document.cancel_execution") + } + + def update_perspective(old_id: Document.Version_ID, new_id: Document.Version_ID, + name: Document.Node.Name, perspective: Command.Perspective) + { + val ids = + { import XML.Encode._ + list(long)(perspective.commands.map(_.id)) } + + input("Document.update_perspective", Document.ID(old_id), Document.ID(new_id), + name.node, YXML.string_of_body(ids)) + } + + def update(old_id: Document.Version_ID, new_id: Document.Version_ID, + edits: List[Document.Edit_Command]) + { + val edits_yxml = + { import XML.Encode._ + def id: T[Command] = (cmd => long(cmd.id)) + def encode_edit(dir: String) + : T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] = + variant(List( + { case Document.Node.Clear() => (Nil, Nil) }, + { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) }, + { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) => + (Nil, + triple(pair(string, string), list(string), list(pair(string, bool)))( + (dir, a), b, c)) }, + { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) }, + { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) })) + def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) => + { + val (name, edit) = node_edit + val dir = Isabelle_System.posix_path(name.dir) + pair(string, encode_edit(dir))(name.node, edit) + }) + YXML.string_of_body(encode(edits)) } + input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml) + } + + def remove_versions(versions: List[Document.Version]) + { + val versions_yxml = + { import XML.Encode._ + YXML.string_of_body(list(long)(versions.map(_.id))) } + input("Document.remove_versions", versions_yxml) + } + + + /* method invocation service */ + + def invoke_scala(id: String, tag: Invoke_Scala.Tag.Value, res: String) + { + input("Document.invoke_scala", id, tag.toString, res) + } +} diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Dec 01 20:52:16 2011 +0100 +++ b/src/Pure/ROOT.ML Thu Dec 01 20:54:48 2011 +0100 @@ -270,7 +270,7 @@ use "System/system_channel.ML"; use "System/isabelle_process.ML"; use "System/invoke_scala.ML"; -use "PIDE/isabelle_document.ML"; +use "PIDE/protocol.ML"; use "System/isar.ML"; diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Thu Dec 01 20:52:16 2011 +0100 +++ b/src/Pure/System/isabelle_process.scala Thu Dec 01 20:54:48 2011 +0100 @@ -58,7 +58,7 @@ def is_status = kind == Isabelle_Markup.STATUS def is_report = kind == Isabelle_Markup.REPORT def is_raw = kind == Isabelle_Markup.RAW - def is_ready = Isabelle_Document.is_ready(message) + def is_ready = Protocol.is_ready(message) def is_syslog = is_init || is_exit || is_system || is_ready || is_stderr override def toString: String = @@ -100,7 +100,7 @@ if (kind == Isabelle_Markup.RAW) receiver(new Result(XML.Elem(Markup(kind, props), body))) else { - val msg = XML.Elem(Markup(kind, props), Isabelle_Document.clean_message(body)) + val msg = XML.Elem(Markup(kind, props), Protocol.clean_message(body)) receiver(new Result(xml_cache.cache_tree(msg).asInstanceOf[XML.Elem])) } } diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Dec 01 20:52:16 2011 +0100 +++ b/src/Pure/System/session.scala Thu Dec 01 20:54:48 2011 +0100 @@ -211,7 +211,7 @@ def cancel() { timer.cancel() } } - var prover: Option[Isabelle_Process with Isabelle_Document] = None + var prover: Option[Isabelle_Process with Protocol] = None /* delayed command changes */ @@ -365,7 +365,7 @@ } case Isabelle_Markup.Assign_Execs if result.is_raw => XML.content(result.body).mkString match { - case Isabelle_Document.Assign(id, assign) => + case Protocol.Assign(id, assign) => try { handle_assign(id, assign) } catch { case _: Document.State.Fail => bad_result(result) } case _ => bad_result(result) @@ -378,7 +378,7 @@ } case Isabelle_Markup.Removed_Versions if result.is_raw => XML.content(result.body).mkString match { - case Isabelle_Document.Removed(removed) => + case Protocol.Removed(removed) => try { handle_removed(removed) } catch { case _: Document.State.Fail => bad_result(result) } case _ => bad_result(result) @@ -429,8 +429,7 @@ case Start(timeout, args) if prover.isEmpty => if (phase == Session.Inactive || phase == Session.Failed) { phase = Session.Startup - prover = - Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Isabelle_Document) + prover = Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Protocol) } case Stop => diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Pure/build-jars --- a/src/Pure/build-jars Thu Dec 01 20:52:16 2011 +0100 +++ b/src/Pure/build-jars Thu Dec 01 20:54:48 2011 +0100 @@ -31,10 +31,10 @@ PIDE/blob.scala PIDE/command.scala PIDE/document.scala - PIDE/isabelle_document.scala PIDE/isabelle_markup.scala PIDE/markup.scala PIDE/markup_tree.scala + PIDE/protocol.scala PIDE/text.scala PIDE/xml.scala PIDE/yxml.scala diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Tools/jEdit/src/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Thu Dec 01 20:52:16 2011 +0100 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Thu Dec 01 20:54:48 2011 +0100 @@ -60,7 +60,7 @@ snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))( Markup_Tree.Select[Hyperlink]( { - // FIXME Isabelle_Document.Hyperlink extractor + // FIXME Protocol.Hyperlink extractor case Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)) if (props.find( diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Thu Dec 01 20:52:16 2011 +0100 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Thu Dec 01 20:54:48 2011 +0100 @@ -61,9 +61,9 @@ val state = snapshot.command_state(command) if (snapshot.is_outdated) Some(outdated_color) else - Isabelle_Document.command_status(state.status) match { - case Isabelle_Document.Forked(i) if i > 0 => Some(running1_color) - case Isabelle_Document.Unprocessed => Some(unprocessed1_color) + Protocol.command_status(state.status) match { + case Protocol.Forked(i) if i > 0 => Some(running1_color) + case Protocol.Unprocessed => Some(unprocessed1_color) case _ => None } } @@ -73,13 +73,13 @@ val state = snapshot.command_state(command) if (snapshot.is_outdated) None else - Isabelle_Document.command_status(state.status) match { - case Isabelle_Document.Forked(i) => if (i > 0) Some(running_color) else None - case Isabelle_Document.Unprocessed => Some(unprocessed_color) - case Isabelle_Document.Failed => Some(error_color) - case Isabelle_Document.Finished => - if (state.results.exists(r => Isabelle_Document.is_error(r._2))) Some(error_color) - else if (state.results.exists(r => Isabelle_Document.is_warning(r._2))) Some(warning_color) + Protocol.command_status(state.status) match { + case Protocol.Forked(i) => if (i > 0) Some(running_color) else None + case Protocol.Unprocessed => Some(unprocessed_color) + case Protocol.Failed => Some(error_color) + case Protocol.Finished => + if (state.results.exists(r => Protocol.is_error(r._2))) Some(error_color) + else if (state.results.exists(r => Protocol.is_warning(r._2))) Some(warning_color) else None } } diff -r ccf2cbe86d70 -r b4e7b9968e60 src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Thu Dec 01 20:52:16 2011 +0100 +++ b/src/Tools/jEdit/src/session_dockable.scala Thu Dec 01 20:54:48 2011 +0100 @@ -94,7 +94,7 @@ /* component state -- owned by Swing thread */ - private var nodes_status: Map[Document.Node.Name, Isabelle_Document.Node_Status] = Map.empty + private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty private object Node_Renderer_Component extends Label { @@ -152,7 +152,7 @@ for { name <- nodes node <- snapshot.version.nodes.get(name) - val status = Isabelle_Document.node_status(snapshot.state, snapshot.version, node) + val status = Protocol.node_status(snapshot.state, snapshot.version, node) } nodes_status1 += (name -> status) if (nodes_status != nodes_status1) {