# HG changeset patch # User wenzelm # Date 1263247205 -3600 # Node ID e596a0b71f3cff52f5153e424fb3e94d6246c46d # Parent e10547372c41dab2e08b2495a9a11d951600c14b incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser); diff -r e10547372c41 -r e596a0b71f3c src/Pure/General/xml.scala --- 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) diff -r e10547372c41 -r e596a0b71f3c src/Pure/System/session.scala --- /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] +} diff -r e10547372c41 -r e596a0b71f3c src/Pure/Thy/change.scala --- /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 diff -r e10547372c41 -r e596a0b71f3c src/Pure/Thy/command.scala --- /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) "" else "" + + + /* 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) + } +} diff -r e10547372c41 -r e596a0b71f3c src/Pure/Thy/document.scala --- /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) + } +} diff -r e10547372c41 -r e596a0b71f3c src/Pure/Thy/markup_node.scala --- /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) + } +} diff -r e10547372c41 -r e596a0b71f3c src/Pure/Thy/state.scala --- /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 + } +} diff -r e10547372c41 -r e596a0b71f3c src/Pure/build-jars --- 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 diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/jedit/document_model.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 diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/jedit/document_view.scala --- 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} diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/jedit/html_panel.scala --- /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 = + """ + + + + + + + +""" + + + /* 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) } +} diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- 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 diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- 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") { diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/jedit/output_dockable.scala --- 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 diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/jedit/plugin.scala --- 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 diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/proofdocument/change.scala --- 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 diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/proofdocument/command.scala --- 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) "" else "" - - - /* 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) - } -} diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/proofdocument/document.scala --- 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) - } -} diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/proofdocument/html_panel.scala --- 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 = - """ - - - - - - - -""" - - - /* 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) } -} diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/proofdocument/markup_node.scala --- 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) - } -} diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/proofdocument/session.scala --- 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] -} diff -r e10547372c41 -r e596a0b71f3c src/Tools/jEdit/src/proofdocument/state.scala --- 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 - } -}