incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
--- a/src/Pure/General/xml.scala Mon Jan 11 22:44:21 2010 +0100
+++ b/src/Pure/General/xml.scala Mon Jan 11 23:00:05 2010 +0100
@@ -10,8 +10,6 @@
import java.lang.ref.WeakReference
import javax.xml.parsers.DocumentBuilderFactory
-import org.w3c.dom.{Node, Document}
-
object XML
{
@@ -151,15 +149,15 @@
/* document object model (W3C DOM) */
- def get_data(node: Node): Option[XML.Tree] =
+ def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
node.getUserData(Markup.DATA) match {
case tree: XML.Tree => Some(tree)
case _ => None
}
- def document_node(doc: Document, tree: Tree): Node =
+ def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
{
- def DOM(tr: Tree): Node = tr match {
+ def DOM(tr: Tree): org.w3c.dom.Node = tr match {
case Elem(Markup.DATA, Nil, List(data, t)) =>
val node = DOM(t)
node.setUserData(Markup.DATA, data, null)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/session.scala Mon Jan 11 23:00:05 2010 +0100
@@ -0,0 +1,250 @@
+/*
+ * Isabelle session, potentially with running prover
+ *
+ * @author Makarius
+ */
+
+package isabelle
+
+
+import scala.actors.TIMEOUT
+import scala.actors.Actor._
+
+
+object Session
+{
+ /* events */
+
+ case object Global_Settings
+
+
+ /* managed entities */
+
+ type Entity_ID = String
+
+ trait Entity
+ {
+ val id: Entity_ID
+ def consume(session: Session, message: XML.Tree): Unit
+ }
+}
+
+
+class Session(system: Isabelle_System)
+{
+ /* pervasive event buses */
+
+ val global_settings = new Event_Bus[Session.Global_Settings.type]
+ val raw_results = new Event_Bus[Isabelle_Process.Result]
+ val results = new Event_Bus[Command]
+
+ val command_change = new Event_Bus[Command]
+
+
+ /* unique ids */
+
+ private var id_count: BigInt = 0
+ def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
+
+
+
+ /** main actor **/
+
+ @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
+ }
+
+ private case class Start(timeout: Int, args: List[String])
+ private case object Stop
+ private case class Begin_Document(path: String)
+
+ private val session_actor = actor {
+
+ var prover: Isabelle_Process with Isar_Document = null
+
+ def register(entity: Session.Entity) { entities += (entity.id -> entity) }
+
+ var documents = Map[Isar_Document.Document_ID, Document]()
+ def register_document(doc: Document) { documents += (doc.id -> doc) }
+
+
+ /* document changes */
+
+ def handle_change(change: Change)
+ {
+ 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)
+ })
+ }
+ register_document(doc)
+ prover.edit_document(change.parent.get.id, doc.id, id_changes)
+ }
+
+
+ /* prover results */
+
+ def bad_result(result: Isabelle_Process.Result)
+ {
+ System.err.println("Ignoring prover result: " + result)
+ }
+
+ def handle_result(result: Isabelle_Process.Result)
+ {
+ raw_results.event(result)
+
+ val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
+ val target: Option[Session.Entity] =
+ target_id match {
+ case None => None
+ case Some(id) => lookup_entity(id)
+ }
+ if (target.isDefined) target.get.consume(this, result.message)
+ else if (result.kind == Isabelle_Process.Kind.STATUS) {
+ // global status message
+ result.body match {
+
+ // document state assigment
+ case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
+ documents.get(target_id.get) match {
+ case Some(doc) =>
+ val states =
+ for {
+ XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, 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)
+ }
+
+ // command and keyword declarations
+ case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
+ syntax += (name, kind)
+ case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
+ syntax += name
+
+ case _ => if (!result.is_ready) bad_result(result)
+ }
+ }
+ else if (result.kind == Isabelle_Process.Kind.EXIT)
+ prover = null
+ else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw)
+ bad_result(result)
+ }
+
+
+ /* prover startup */
+
+ def startup_error(): String =
+ {
+ val buf = new StringBuilder
+ while (
+ receiveWithin(0) {
+ case result: Isabelle_Process.Result =>
+ if (result.is_raw) {
+ for (text <- XML.content(result.message))
+ buf.append(text)
+ }
+ true
+ case TIMEOUT => false
+ }) {}
+ buf.toString
+ }
+
+ def prover_startup(timeout: Int): Option[String] =
+ {
+ receiveWithin(timeout) {
+ case result: Isabelle_Process.Result
+ if result.kind == Isabelle_Process.Kind.INIT =>
+ while (receive {
+ case result: Isabelle_Process.Result =>
+ handle_result(result); !result.is_ready
+ }) {}
+ None
+
+ case result: Isabelle_Process.Result
+ if result.kind == Isabelle_Process.Kind.EXIT =>
+ Some(startup_error())
+
+ case TIMEOUT => // FIXME clarify
+ prover.kill; Some(startup_error())
+ }
+ }
+
+
+ /* main loop */
+
+ val xml_cache = new XML.Cache(131071)
+
+ loop {
+ react {
+ case Start(timeout, args) =>
+ if (prover == null) {
+ prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
+ val origin = sender
+ val opt_err = prover_startup(timeout)
+ if (opt_err.isDefined) prover = null
+ origin ! opt_err
+ }
+ else reply(None)
+
+ case Stop => // FIXME clarify; synchronous
+ if (prover != null) {
+ prover.kill
+ 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)
+
+ case result: Isabelle_Process.Result =>
+ handle_result(result.cache(xml_cache))
+
+ case bad if prover != null =>
+ System.err.println("session_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+
+ /* main methods */
+
+ def start(timeout: Int, args: List[String]): Option[String] =
+ (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
+
+ 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]
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/change.scala Mon Jan 11 23:00:05 2010 +0100
@@ -0,0 +1,42 @@
+/*
+ * Changes of plain text
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle
+
+
+class Change(
+ val id: Isar_Document.Document_ID,
+ val parent: Option[Change],
+ val edits: List[Text_Edit],
+ val result: Future[(List[Document.Edit], 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 edit(session: Session, edits: List[Text_Edit]): Change =
+ {
+ val new_id = session.create_id()
+ val result: Future[(List[Document.Edit], Document)] =
+ Future.fork {
+ val old_doc = join_document
+ old_doc.await_assignment
+ Document.text_edits(session, old_doc, new_id, edits)
+ }
+ new Change(new_id, Some(this), edits, result)
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/command.scala Mon Jan 11 23:00:05 2010 +0100
@@ -0,0 +1,100 @@
+/*
+ * Prover commands with semantic state
+ *
+ * @author Johannes Hölzl, TU Munich
+ * @author Fabian Immler, TU Munich
+ */
+
+package isabelle
+
+
+import scala.actors.Actor, Actor._
+import scala.collection.mutable
+
+
+object Command
+{
+ object Status extends Enumeration
+ {
+ val UNPROCESSED = Value("UNPROCESSED")
+ val FINISHED = Value("FINISHED")
+ val FAILED = Value("FAILED")
+ }
+
+ case class HighlightInfo(highlight: String) { override def toString = highlight }
+ case class TypeInfo(ty: String)
+ case class RefInfo(file: Option[String], line: Option[Int],
+ command_id: Option[String], offset: Option[Int])
+}
+
+
+class Command(
+ val id: Isar_Document.Command_ID,
+ val span: Thy_Syntax.Span)
+ extends Session.Entity
+{
+ /* classification */
+
+ def is_command: Boolean = !span.isEmpty && span.first.is_command
+ def is_ignored: Boolean = span.forall(_.is_ignored)
+ def is_malformed: Boolean = !is_command && !is_ignored
+
+ def name: String = if (is_command) span.first.content else ""
+ override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
+
+
+ /* source text */
+
+ val source: String = span.map(_.source).mkString
+ def source(i: Int, j: Int): String = source.substring(i, j)
+ def length: Int = source.length
+
+ 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(session: Session, message: XML.Tree)
+ private case object Assign
+
+ private val accumulator = actor {
+ var assigned = false
+ loop {
+ react {
+ case Consume(session: Session, message: XML.Tree) if !assigned =>
+ state = state.+(session, message)
+
+ case Assign =>
+ assigned = true // single assignment
+ reply(())
+
+ case bad => System.err.println("command accumulator: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
+
+ def assign_state(state_id: Isar_Document.State_ID): Command =
+ {
+ val cmd = new Command(state_id, span)
+ 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)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/document.scala Mon Jan 11 23:00:05 2010 +0100
@@ -0,0 +1,197 @@
+/*
+ * Document as editable list of commands
+ *
+ * @author Makarius
+ */
+
+package isabelle
+
+
+object Document
+{
+ /* command start positions */
+
+ def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
+ {
+ var offset = 0
+ for (cmd <- commands.elements) yield {
+ val start = offset
+ offset += cmd.length
+ (cmd, start)
+ }
+ }
+
+
+ /* empty document */
+
+ def empty(id: Isar_Document.Document_ID): Document =
+ {
+ val doc = new Document(id, Linear_Set(), Map())
+ doc.assign_states(Nil)
+ doc
+ }
+
+
+ // FIXME
+ var phase0: List[Text_Edit] = null
+ var phase1: Linear_Set[Command] = null
+ var phase2: Linear_Set[Command] = null
+ var phase3: List[Edit] = null
+
+
+
+ /** 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) =
+ {
+ require(old_doc.assignment.is_finished)
+
+
+ /* unparsed dummy commands */
+
+ def unparsed(source: String) =
+ new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
+
+ def is_unparsed(command: Command) = command.id == null
+
+ assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
+
+
+ /* phase 1: edit individual command source */
+
+ def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
+ {
+ eds match {
+ case e :: es =>
+ command_starts(commands).find { // FIXME relative search!
+ 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)
+
+ case Some((cmd, cmd_start)) =>
+ edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
+
+ case None =>
+ require(e.is_insert && e.start == 0)
+ edit_text(es, commands.insert_after(None, unparsed(e.text)))
+ }
+ case Nil => commands
+ }
+ }
+
+
+ /* phase 2: recover command spans */
+
+ def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
+ {
+ // FIXME relative search!
+ commands.elements.find(is_unparsed) match {
+ case Some(first_unparsed) =>
+ val prefix = commands.prev(first_unparsed)
+ val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
+ val suffix = commands.next(body.last)
+
+ val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
+ val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
+
+ val (before_edit, spans1) =
+ if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
+ (prefix, spans0.tail)
+ else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
+
+ val (after_edit, spans2) =
+ if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
+ (suffix, spans1.take(spans1.length - 1))
+ else (if (suffix.isDefined) commands.next(suffix.get) else None, 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)
+ parse_spans(new_commands)
+
+ case None => commands
+ }
+ }
+
+
+ /* phase 3: resulting document edits */
+
+ val result = Library.timeit("text_edits") {
+ val commands0 = old_doc.commands
+ val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
+ val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
+
+ val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
+ val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
+
+ val doc_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
+
+ phase0 = edits
+ phase1 = commands1
+ phase2 = commands2
+ phase3 = doc_edits
+
+ (doc_edits, new Document(new_id, commands2, former_states))
+ }
+ result
+ }
+}
+
+
+class Document(
+ val id: Isar_Document.Document_ID,
+ val commands: Linear_Set[Command],
+ former_states: Map[Command, Command])
+{
+ /* command ranges */
+
+ def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
+
+ def command_start(cmd: Command): Option[Int] =
+ command_starts.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(i: Int, j: Int): Iterator[(Command, Int)] =
+ command_range(i) takeWhile { case (_, start) => start < j }
+
+ def command_at(i: Int): Option[(Command, Int)] =
+ {
+ val range = command_range(i)
+ if (range.hasNext) Some(range.next) else None
+ }
+
+
+ /* command state assignment */
+
+ val assignment = Future.promise[Map[Command, Command]]
+ def await_assignment { assignment.join }
+
+ @volatile private var tmp_states = former_states
+ private val time0 = System.currentTimeMillis
+
+ def assign_states(new_states: List[(Command, Command)])
+ {
+ assignment.fulfill(tmp_states ++ new_states)
+ tmp_states = Map()
+ System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
+ }
+
+ def current_state(cmd: Command): Option[State] =
+ {
+ require(assignment.is_finished)
+ (assignment.join).get(cmd).map(_.current_state)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/markup_node.scala Mon Jan 11 23:00:05 2010 +0100
@@ -0,0 +1,111 @@
+/*
+ * Document markup nodes, with connection to Swing tree model
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle
+
+
+import javax.swing.tree.DefaultMutableTreeNode
+
+
+
+class Markup_Node(val start: Int, val stop: Int, val info: Any)
+{
+ def fits_into(that: Markup_Node): Boolean =
+ that.start <= this.start && this.stop <= that.stop
+}
+
+
+class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
+{
+ def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
+
+ private def add(branch: Markup_Tree) = // FIXME avoid sort
+ set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
+
+ private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
+
+ def + (new_tree: Markup_Tree): Markup_Tree =
+ {
+ val new_node = new_tree.node
+ if (new_node fits_into node) {
+ var inserted = false
+ val new_branches =
+ branches.map(branch =>
+ if ((new_node fits_into branch.node) && !inserted) {
+ inserted = true
+ branch + new_tree
+ }
+ else branch)
+ if (!inserted) {
+ // new_tree did not fit into children of this
+ // -> insert between this and its branches
+ val fitting = branches filter(_.node fits_into new_node)
+ (this remove fitting) add ((new_tree /: fitting)(_ + _))
+ }
+ else set_branches(new_branches)
+ }
+ else {
+ System.err.println("ignored nonfitting markup: " + new_node)
+ this
+ }
+ }
+
+ def flatten: List[Markup_Node] =
+ {
+ var next_x = node.start
+ if (branches.isEmpty) List(this.node)
+ else {
+ val filled_gaps =
+ for {
+ child <- branches
+ markups =
+ if (next_x < child.node.start)
+ new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
+ else child.flatten
+ update = (next_x = child.node.stop)
+ markup <- markups
+ } yield markup
+ if (next_x < node.stop)
+ filled_gaps + new Markup_Node(next_x, node.stop, node.info)
+ else filled_gaps
+ }
+ }
+}
+
+
+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)
+
+ def + (new_tree: Markup_Tree): Markup_Text =
+ new Markup_Text((root + new_tree).branches, content)
+
+ def filter(pred: Markup_Node => Boolean): Markup_Text =
+ {
+ def filt(tree: Markup_Tree): List[Markup_Tree] =
+ {
+ val branches = tree.branches.flatMap(filt(_))
+ if (pred(tree.node)) List(tree.set_branches(branches))
+ else branches
+ }
+ new Markup_Text(markup.flatMap(filt(_)), content)
+ }
+
+ def flatten: List[Markup_Node] = markup.flatten(_.flatten)
+
+ def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
+ {
+ def swing(tree: Markup_Tree): DefaultMutableTreeNode =
+ {
+ val node = swing_node(tree.node)
+ tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
+ node
+ }
+ swing(root)
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/state.scala Mon Jan 11 23:00:05 2010 +0100
@@ -0,0 +1,117 @@
+/*
+ * Accumulating results from prover
+ *
+ * @author Fabian Immler, TU Munich
+ * @author Makarius
+ */
+
+package isabelle
+
+
+class State(
+ val command: Command,
+ val status: Command.Status.Value,
+ val rev_results: List[XML.Tree],
+ val markup_root: Markup_Text)
+{
+ def this(command: Command) =
+ this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
+
+
+ /* content */
+
+ private def set_status(st: Command.Status.Value): State =
+ new State(command, st, rev_results, markup_root)
+
+ private def add_result(res: XML.Tree): State =
+ new State(command, status, res :: rev_results, markup_root)
+
+ private def add_markup(node: Markup_Tree): State =
+ new State(command, status, rev_results, markup_root + node)
+
+ lazy val results = rev_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 + (session: Session, message: XML.Tree): State =
+ {
+ val changed: State =
+ message match {
+ case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
+ (this /: elems)((state, elem) =>
+ elem match {
+ case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
+ case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
+ case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
+ case XML.Elem(kind, atts, body) =>
+ val (begin, end) = Position.get_offsets(atts)
+ if (begin.isEmpty || end.isEmpty) state
+ else if (kind == Markup.ML_TYPING) {
+ val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
+ state.add_markup(
+ command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
+ }
+ else if (kind == Markup.ML_REF) {
+ body match {
+ case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+ state.add_markup(command.markup_node(
+ begin.get - 1, end.get - 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.get - 1, end.get - 1, Command.HighlightInfo(kind)))
+ }
+ case _ =>
+ System.err.println("ignored status report: " + elem)
+ state
+ })
+ case _ => add_result(message)
+ }
+ if (!(this eq changed)) session.command_change.event(command)
+ changed
+ }
+}
--- a/src/Pure/build-jars Mon Jan 11 22:44:21 2010 +0100
+++ b/src/Pure/build-jars Mon Jan 11 23:00:05 2010 +0100
@@ -45,10 +45,16 @@
System/isabelle_syntax.scala
System/isabelle_system.scala
System/platform.scala
+ System/session.scala
System/session_manager.scala
System/standard_system.scala
+ Thy/change.scala
+ Thy/command.scala
Thy/completion.scala
+ Thy/document.scala
Thy/html.scala
+ Thy/markup_node.scala
+ Thy/state.scala
Thy/text_edit.scala
Thy/thy_header.scala
Thy/thy_syntax.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 11 22:44:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 11 23:00:05 2010 +0100
@@ -8,8 +8,6 @@
package isabelle.jedit
-import isabelle.proofdocument.{Change, Command, Document, Session}
-
import scala.actors.Actor, Actor._
import scala.collection.mutable
--- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 22:44:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 23:00:05 2010 +0100
@@ -8,8 +8,6 @@
package isabelle.jedit
-import isabelle.proofdocument.{Command, Document, Session}
-
import scala.actors.Actor._
import java.awt.event.{MouseAdapter, MouseEvent}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala Mon Jan 11 23:00:05 2010 +0100
@@ -0,0 +1,140 @@
+/*
+ * HTML panel based on Lobo/Cobra
+ *
+ * @author Makarius
+ */
+
+package isabelle.jedit
+
+
+import java.io.StringReader
+import java.awt.{BorderLayout, Dimension}
+import java.awt.event.MouseEvent
+
+import javax.swing.{JButton, JPanel, JScrollPane}
+import java.util.logging.{Logger, Level}
+
+import org.w3c.dom.html2.HTMLElement
+
+import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
+import org.lobobrowser.html.gui.HtmlPanel
+import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
+import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
+
+import scala.io.Source
+import scala.actors.Actor._
+
+
+object HTML_Panel
+{
+ sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
+ case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
+ case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
+ case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
+ case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
+ case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
+}
+
+
+class HTML_Panel(
+ sys: Isabelle_System,
+ initial_font_size: Int,
+ handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
+{
+ // global logging
+ Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
+
+
+ /* document template */
+
+ private def try_file(name: String): String =
+ {
+ val file = sys.platform_file(name)
+ if (file.isFile) Source.fromFile(file).mkString else ""
+ }
+
+ private def template(font_size: Int): String =
+ """<?xml version="1.0" encoding="utf-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<style media="all" type="text/css">
+""" +
+ try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
+ try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
+ "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
+"""
+</style>
+</head>
+<body/>
+</html>
+"""
+
+
+ /* actor with local state */
+
+ private val ucontext = new SimpleUserAgentContext
+
+ private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
+ {
+ private def handle(event: HTML_Panel.Event): Boolean =
+ if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
+ else false
+
+ override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
+ handle(HTML_Panel.Context_Menu(elem, event))
+ override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
+ handle(HTML_Panel.Mouse_Click(elem, event))
+ override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
+ handle(HTML_Panel.Double_Click(elem, event))
+ override def onMouseOver(elem: HTMLElement, event: MouseEvent)
+ { handle(HTML_Panel.Mouse_Over(elem, event)) }
+ override def onMouseOut(elem: HTMLElement, event: MouseEvent)
+ { handle(HTML_Panel.Mouse_Out(elem, event)) }
+ }
+
+ private val builder = new DocumentBuilderImpl(ucontext, rcontext)
+
+ private case class Init(font_size: Int)
+ private case class Render(body: List[XML.Tree])
+
+ private val main_actor = actor {
+ // crude double buffering
+ var doc1: org.w3c.dom.Document = null
+ var doc2: org.w3c.dom.Document = null
+
+ loop {
+ react {
+ case Init(font_size) =>
+ val src = template(font_size)
+ def parse() =
+ builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
+ doc1 = parse()
+ doc2 = parse()
+ Swing_Thread.now { setDocument(doc1, rcontext) }
+
+ case Render(body) =>
+ val doc = doc2
+ val node =
+ XML.document_node(doc,
+ XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
+ doc.removeChild(doc.getLastChild())
+ doc.appendChild(node)
+ doc2 = doc1
+ doc1 = doc
+ Swing_Thread.now { setDocument(doc1, rcontext) }
+
+ case bad => System.err.println("main_actor: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ main_actor ! Init(initial_font_size)
+
+
+ /* main method wrappers */
+
+ def init(font_size: Int) { main_actor ! Init(font_size) }
+ def render(body: List[XML.Tree]) { main_actor ! Render(body) }
+}
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 22:44:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 23:00:05 2010 +0100
@@ -6,7 +6,6 @@
package isabelle.jedit
-import isabelle.proofdocument.Command
import java.io.File
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 22:44:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 23:00:05 2010 +0100
@@ -19,8 +19,6 @@
import errorlist.DefaultErrorSource
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
-import isabelle.proofdocument.{Command, Markup_Node, Document}
-
class Isabelle_Sidekick extends SideKickParser("isabelle")
{
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 22:44:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 23:00:05 2010 +0100
@@ -7,8 +7,6 @@
package isabelle.jedit
-import isabelle.proofdocument.{Command, HTML_Panel, Session}
-
import scala.actors.Actor._
import javax.swing.JPanel
--- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Jan 11 22:44:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Jan 11 23:00:05 2010 +0100
@@ -9,8 +9,6 @@
package isabelle.jedit
-import isabelle.proofdocument.Session
-
import java.io.{FileInputStream, IOException}
import java.awt.Font
import javax.swing.JTextArea
--- a/src/Tools/jEdit/src/proofdocument/change.scala Mon Jan 11 22:44:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-/*
- * Changes of plain text
- *
- * @author Fabian Immler, TU Munich
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-
-class Change(
- val id: Isar_Document.Document_ID,
- val parent: Option[Change],
- val edits: List[Text_Edit],
- val result: Future[(List[Document.Edit], 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 edit(session: Session, edits: List[Text_Edit]): Change =
- {
- val new_id = session.create_id()
- val result: Future[(List[Document.Edit], Document)] =
- Future.fork {
- val old_doc = join_document
- old_doc.await_assignment
- Document.text_edits(session, old_doc, new_id, edits)
- }
- new Change(new_id, Some(this), edits, result)
- }
-}
\ No newline at end of file
--- a/src/Tools/jEdit/src/proofdocument/command.scala Mon Jan 11 22:44:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-/*
- * Prover commands with semantic state
- *
- * @author Johannes Hölzl, TU Munich
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.proofdocument
-
-
-import scala.actors.Actor, Actor._
-import scala.collection.mutable
-
-import isabelle.jedit.Isabelle
-
-
-object Command
-{
- object Status extends Enumeration
- {
- val UNPROCESSED = Value("UNPROCESSED")
- val FINISHED = Value("FINISHED")
- val FAILED = Value("FAILED")
- }
-
- case class HighlightInfo(highlight: String) { override def toString = highlight }
- case class TypeInfo(ty: String)
- case class RefInfo(file: Option[String], line: Option[Int],
- command_id: Option[String], offset: Option[Int])
-}
-
-
-class Command(
- val id: Isar_Document.Command_ID,
- val span: Thy_Syntax.Span)
- extends Session.Entity
-{
- /* classification */
-
- def is_command: Boolean = !span.isEmpty && span.first.is_command
- def is_ignored: Boolean = span.forall(_.is_ignored)
- def is_malformed: Boolean = !is_command && !is_ignored
-
- def name: String = if (is_command) span.first.content else ""
- override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
-
-
- /* source text */
-
- val source: String = span.map(_.source).mkString
- def source(i: Int, j: Int): String = source.substring(i, j)
- def length: Int = source.length
-
- 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(session: Session, message: XML.Tree)
- private case object Assign
-
- private val accumulator = actor {
- var assigned = false
- loop {
- react {
- case Consume(session: Session, message: XML.Tree) if !assigned =>
- state = state.+(session, message)
-
- case Assign =>
- assigned = true // single assignment
- reply(())
-
- case bad => System.err.println("command accumulator: ignoring bad message " + bad)
- }
- }
- }
-
- def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
-
- def assign_state(state_id: Isar_Document.State_ID): Command =
- {
- val cmd = new Command(state_id, span)
- 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)
- }
-}
--- a/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 11 22:44:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,197 +0,0 @@
-/*
- * Document as editable list of commands
- *
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-
-object Document
-{
- /* command start positions */
-
- def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
- {
- var offset = 0
- for (cmd <- commands.elements) yield {
- val start = offset
- offset += cmd.length
- (cmd, start)
- }
- }
-
-
- /* empty document */
-
- def empty(id: Isar_Document.Document_ID): Document =
- {
- val doc = new Document(id, Linear_Set(), Map())
- doc.assign_states(Nil)
- doc
- }
-
-
- // FIXME
- var phase0: List[Text_Edit] = null
- var phase1: Linear_Set[Command] = null
- var phase2: Linear_Set[Command] = null
- var phase3: List[Edit] = null
-
-
-
- /** 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) =
- {
- require(old_doc.assignment.is_finished)
-
-
- /* unparsed dummy commands */
-
- def unparsed(source: String) =
- new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
-
- def is_unparsed(command: Command) = command.id == null
-
- assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
-
-
- /* phase 1: edit individual command source */
-
- def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
- {
- eds match {
- case e :: es =>
- command_starts(commands).find { // FIXME relative search!
- 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)
-
- case Some((cmd, cmd_start)) =>
- edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
-
- case None =>
- require(e.is_insert && e.start == 0)
- edit_text(es, commands.insert_after(None, unparsed(e.text)))
- }
- case Nil => commands
- }
- }
-
-
- /* phase 2: recover command spans */
-
- def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
- {
- // FIXME relative search!
- commands.elements.find(is_unparsed) match {
- case Some(first_unparsed) =>
- val prefix = commands.prev(first_unparsed)
- val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
- val suffix = commands.next(body.last)
-
- val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
- val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
-
- val (before_edit, spans1) =
- if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
- (prefix, spans0.tail)
- else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
-
- val (after_edit, spans2) =
- if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
- (suffix, spans1.take(spans1.length - 1))
- else (if (suffix.isDefined) commands.next(suffix.get) else None, 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)
- parse_spans(new_commands)
-
- case None => commands
- }
- }
-
-
- /* phase 3: resulting document edits */
-
- val result = Library.timeit("text_edits") {
- val commands0 = old_doc.commands
- val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
- val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
-
- val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
- val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
-
- val doc_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
-
- phase0 = edits
- phase1 = commands1
- phase2 = commands2
- phase3 = doc_edits
-
- (doc_edits, new Document(new_id, commands2, former_states))
- }
- result
- }
-}
-
-
-class Document(
- val id: Isar_Document.Document_ID,
- val commands: Linear_Set[Command],
- former_states: Map[Command, Command])
-{
- /* command ranges */
-
- def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
-
- def command_start(cmd: Command): Option[Int] =
- command_starts.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(i: Int, j: Int): Iterator[(Command, Int)] =
- command_range(i) takeWhile { case (_, start) => start < j }
-
- def command_at(i: Int): Option[(Command, Int)] =
- {
- val range = command_range(i)
- if (range.hasNext) Some(range.next) else None
- }
-
-
- /* command state assignment */
-
- val assignment = Future.promise[Map[Command, Command]]
- def await_assignment { assignment.join }
-
- @volatile private var tmp_states = former_states
- private val time0 = System.currentTimeMillis
-
- def assign_states(new_states: List[(Command, Command)])
- {
- assignment.fulfill(tmp_states ++ new_states)
- tmp_states = Map()
- System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
- }
-
- def current_state(cmd: Command): Option[State] =
- {
- require(assignment.is_finished)
- (assignment.join).get(cmd).map(_.current_state)
- }
-}
--- a/src/Tools/jEdit/src/proofdocument/html_panel.scala Mon Jan 11 22:44:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,140 +0,0 @@
-/*
- * HTML panel based on Lobo/Cobra
- *
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-
-import java.io.StringReader
-import java.awt.{BorderLayout, Dimension}
-import java.awt.event.MouseEvent
-
-import javax.swing.{JButton, JPanel, JScrollPane}
-import java.util.logging.{Logger, Level}
-
-import org.w3c.dom.html2.HTMLElement
-
-import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
-import org.lobobrowser.html.gui.HtmlPanel
-import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
-import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
-
-import scala.io.Source
-import scala.actors.Actor._
-
-
-object HTML_Panel
-{
- sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
- case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
- case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
-}
-
-
-class HTML_Panel(
- sys: Isabelle_System,
- initial_font_size: Int,
- handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
-{
- // global logging
- Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
-
-
- /* document template */
-
- private def try_file(name: String): String =
- {
- val file = sys.platform_file(name)
- if (file.isFile) Source.fromFile(file).mkString else ""
- }
-
- private def template(font_size: Int): String =
- """<?xml version="1.0" encoding="utf-8"?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
- "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml">
-<head>
-<style media="all" type="text/css">
-""" +
- try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
- try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
- "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
-"""
-</style>
-</head>
-<body/>
-</html>
-"""
-
-
- /* actor with local state */
-
- private val ucontext = new SimpleUserAgentContext
-
- private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
- {
- private def handle(event: HTML_Panel.Event): Boolean =
- if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
- else false
-
- override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
- handle(HTML_Panel.Context_Menu(elem, event))
- override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
- handle(HTML_Panel.Mouse_Click(elem, event))
- override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
- handle(HTML_Panel.Double_Click(elem, event))
- override def onMouseOver(elem: HTMLElement, event: MouseEvent)
- { handle(HTML_Panel.Mouse_Over(elem, event)) }
- override def onMouseOut(elem: HTMLElement, event: MouseEvent)
- { handle(HTML_Panel.Mouse_Out(elem, event)) }
- }
-
- private val builder = new DocumentBuilderImpl(ucontext, rcontext)
-
- private case class Init(font_size: Int)
- private case class Render(body: List[XML.Tree])
-
- private val main_actor = actor {
- // crude double buffering
- var doc1: org.w3c.dom.Document = null
- var doc2: org.w3c.dom.Document = null
-
- loop {
- react {
- case Init(font_size) =>
- val src = template(font_size)
- def parse() =
- builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
- doc1 = parse()
- doc2 = parse()
- Swing_Thread.now { setDocument(doc1, rcontext) }
-
- case Render(body) =>
- val doc = doc2
- val node =
- XML.document_node(doc,
- XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
- doc.removeChild(doc.getLastChild())
- doc.appendChild(node)
- doc2 = doc1
- doc1 = doc
- Swing_Thread.now { setDocument(doc1, rcontext) }
-
- case bad => System.err.println("main_actor: ignoring bad message " + bad)
- }
- }
- }
-
- main_actor ! Init(initial_font_size)
-
-
- /* main method wrappers */
-
- def init(font_size: Int) { main_actor ! Init(font_size) }
- def render(body: List[XML.Tree]) { main_actor ! Render(body) }
-}
--- a/src/Tools/jEdit/src/proofdocument/markup_node.scala Mon Jan 11 22:44:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-/*
- * Document markup nodes, with connection to Swing tree model
- *
- * @author Fabian Immler, TU Munich
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-
-import javax.swing.tree.DefaultMutableTreeNode
-
-
-
-class Markup_Node(val start: Int, val stop: Int, val info: Any)
-{
- def fits_into(that: Markup_Node): Boolean =
- that.start <= this.start && this.stop <= that.stop
-}
-
-
-class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
-{
- def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
-
- private def add(branch: Markup_Tree) = // FIXME avoid sort
- set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
-
- private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
-
- def + (new_tree: Markup_Tree): Markup_Tree =
- {
- val new_node = new_tree.node
- if (new_node fits_into node) {
- var inserted = false
- val new_branches =
- branches.map(branch =>
- if ((new_node fits_into branch.node) && !inserted) {
- inserted = true
- branch + new_tree
- }
- else branch)
- if (!inserted) {
- // new_tree did not fit into children of this
- // -> insert between this and its branches
- val fitting = branches filter(_.node fits_into new_node)
- (this remove fitting) add ((new_tree /: fitting)(_ + _))
- }
- else set_branches(new_branches)
- }
- else {
- System.err.println("ignored nonfitting markup: " + new_node)
- this
- }
- }
-
- def flatten: List[Markup_Node] =
- {
- var next_x = node.start
- if (branches.isEmpty) List(this.node)
- else {
- val filled_gaps =
- for {
- child <- branches
- markups =
- if (next_x < child.node.start)
- new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
- else child.flatten
- update = (next_x = child.node.stop)
- markup <- markups
- } yield markup
- if (next_x < node.stop)
- filled_gaps + new Markup_Node(next_x, node.stop, node.info)
- else filled_gaps
- }
- }
-}
-
-
-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)
-
- def + (new_tree: Markup_Tree): Markup_Text =
- new Markup_Text((root + new_tree).branches, content)
-
- def filter(pred: Markup_Node => Boolean): Markup_Text =
- {
- def filt(tree: Markup_Tree): List[Markup_Tree] =
- {
- val branches = tree.branches.flatMap(filt(_))
- if (pred(tree.node)) List(tree.set_branches(branches))
- else branches
- }
- new Markup_Text(markup.flatMap(filt(_)), content)
- }
-
- def flatten: List[Markup_Node] = markup.flatten(_.flatten)
-
- def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
- {
- def swing(tree: Markup_Tree): DefaultMutableTreeNode =
- {
- val node = swing_node(tree.node)
- tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
- node
- }
- swing(root)
- }
-}
--- a/src/Tools/jEdit/src/proofdocument/session.scala Mon Jan 11 22:44:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,250 +0,0 @@
-/*
- * Isabelle session, potentially with running prover
- *
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-
-import scala.actors.TIMEOUT
-import scala.actors.Actor._
-
-
-object Session
-{
- /* events */
-
- case object Global_Settings
-
-
- /* managed entities */
-
- type Entity_ID = String
-
- trait Entity
- {
- val id: Entity_ID
- def consume(session: Session, message: XML.Tree): Unit
- }
-}
-
-
-class Session(system: Isabelle_System)
-{
- /* pervasive event buses */
-
- val global_settings = new Event_Bus[Session.Global_Settings.type]
- val raw_results = new Event_Bus[Isabelle_Process.Result]
- val results = new Event_Bus[Command]
-
- val command_change = new Event_Bus[Command]
-
-
- /* unique ids */
-
- private var id_count: BigInt = 0
- def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
-
-
-
- /** main actor **/
-
- @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
- }
-
- private case class Start(timeout: Int, args: List[String])
- private case object Stop
- private case class Begin_Document(path: String)
-
- private val session_actor = actor {
-
- var prover: Isabelle_Process with Isar_Document = null
-
- def register(entity: Session.Entity) { entities += (entity.id -> entity) }
-
- var documents = Map[Isar_Document.Document_ID, Document]()
- def register_document(doc: Document) { documents += (doc.id -> doc) }
-
-
- /* document changes */
-
- def handle_change(change: Change)
- {
- 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)
- })
- }
- register_document(doc)
- prover.edit_document(change.parent.get.id, doc.id, id_changes)
- }
-
-
- /* prover results */
-
- def bad_result(result: Isabelle_Process.Result)
- {
- System.err.println("Ignoring prover result: " + result)
- }
-
- def handle_result(result: Isabelle_Process.Result)
- {
- raw_results.event(result)
-
- val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
- val target: Option[Session.Entity] =
- target_id match {
- case None => None
- case Some(id) => lookup_entity(id)
- }
- if (target.isDefined) target.get.consume(this, result.message)
- else if (result.kind == Isabelle_Process.Kind.STATUS) {
- // global status message
- result.body match {
-
- // document state assigment
- case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
- documents.get(target_id.get) match {
- case Some(doc) =>
- val states =
- for {
- XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, 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)
- }
-
- // command and keyword declarations
- case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
- syntax += (name, kind)
- case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
- syntax += name
-
- case _ => if (!result.is_ready) bad_result(result)
- }
- }
- else if (result.kind == Isabelle_Process.Kind.EXIT)
- prover = null
- else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw)
- bad_result(result)
- }
-
-
- /* prover startup */
-
- def startup_error(): String =
- {
- val buf = new StringBuilder
- while (
- receiveWithin(0) {
- case result: Isabelle_Process.Result =>
- if (result.is_raw) {
- for (text <- XML.content(result.message))
- buf.append(text)
- }
- true
- case TIMEOUT => false
- }) {}
- buf.toString
- }
-
- def prover_startup(timeout: Int): Option[String] =
- {
- receiveWithin(timeout) {
- case result: Isabelle_Process.Result
- if result.kind == Isabelle_Process.Kind.INIT =>
- while (receive {
- case result: Isabelle_Process.Result =>
- handle_result(result); !result.is_ready
- }) {}
- None
-
- case result: Isabelle_Process.Result
- if result.kind == Isabelle_Process.Kind.EXIT =>
- Some(startup_error())
-
- case TIMEOUT => // FIXME clarify
- prover.kill; Some(startup_error())
- }
- }
-
-
- /* main loop */
-
- val xml_cache = new XML.Cache(131071)
-
- loop {
- react {
- case Start(timeout, args) =>
- if (prover == null) {
- prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
- val origin = sender
- val opt_err = prover_startup(timeout)
- if (opt_err.isDefined) prover = null
- origin ! opt_err
- }
- else reply(None)
-
- case Stop => // FIXME clarify; synchronous
- if (prover != null) {
- prover.kill
- 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)
-
- case result: Isabelle_Process.Result =>
- handle_result(result.cache(xml_cache))
-
- case bad if prover != null =>
- System.err.println("session_actor: ignoring bad message " + bad)
- }
- }
- }
-
-
- /* main methods */
-
- def start(timeout: Int, args: List[String]): Option[String] =
- (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
-
- def stop() { session_actor ! Stop }
- def input(change: Change) { session_actor ! change }
-
- def begin_document(path: String): Document =
- (session_actor !? Begin_Document(path)).asInstanceOf[Document]
-}
--- a/src/Tools/jEdit/src/proofdocument/state.scala Mon Jan 11 22:44:21 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-/*
- * Accumulating results from prover
- *
- * @author Fabian Immler, TU Munich
- * @author Makarius
- */
-
-package isabelle.proofdocument
-
-
-class State(
- val command: Command,
- val status: Command.Status.Value,
- val rev_results: List[XML.Tree],
- val markup_root: Markup_Text)
-{
- def this(command: Command) =
- this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
-
-
- /* content */
-
- private def set_status(st: Command.Status.Value): State =
- new State(command, st, rev_results, markup_root)
-
- private def add_result(res: XML.Tree): State =
- new State(command, status, res :: rev_results, markup_root)
-
- private def add_markup(node: Markup_Tree): State =
- new State(command, status, rev_results, markup_root + node)
-
- lazy val results = rev_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 + (session: Session, message: XML.Tree): State =
- {
- val changed: State =
- message match {
- case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
- (this /: elems)((state, elem) =>
- elem match {
- case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
- case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
- case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
- case XML.Elem(kind, atts, body) =>
- val (begin, end) = Position.get_offsets(atts)
- if (begin.isEmpty || end.isEmpty) state
- else if (kind == Markup.ML_TYPING) {
- val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
- state.add_markup(
- command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
- }
- else if (kind == Markup.ML_REF) {
- body match {
- case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
- state.add_markup(command.markup_node(
- begin.get - 1, end.get - 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.get - 1, end.get - 1, Command.HighlightInfo(kind)))
- }
- case _ =>
- System.err.println("ignored status report: " + elem)
- state
- })
- case _ => add_result(message)
- }
- if (!(this eq changed)) session.command_change.event(command)
- changed
- }
-}