incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
1.1 --- a/src/Pure/General/xml.scala Mon Jan 11 22:44:21 2010 +0100
1.2 +++ b/src/Pure/General/xml.scala Mon Jan 11 23:00:05 2010 +0100
1.3 @@ -10,8 +10,6 @@
1.4 import java.lang.ref.WeakReference
1.5 import javax.xml.parsers.DocumentBuilderFactory
1.6
1.7 -import org.w3c.dom.{Node, Document}
1.8 -
1.9
1.10 object XML
1.11 {
1.12 @@ -151,15 +149,15 @@
1.13
1.14 /* document object model (W3C DOM) */
1.15
1.16 - def get_data(node: Node): Option[XML.Tree] =
1.17 + def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
1.18 node.getUserData(Markup.DATA) match {
1.19 case tree: XML.Tree => Some(tree)
1.20 case _ => None
1.21 }
1.22
1.23 - def document_node(doc: Document, tree: Tree): Node =
1.24 + def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
1.25 {
1.26 - def DOM(tr: Tree): Node = tr match {
1.27 + def DOM(tr: Tree): org.w3c.dom.Node = tr match {
1.28 case Elem(Markup.DATA, Nil, List(data, t)) =>
1.29 val node = DOM(t)
1.30 node.setUserData(Markup.DATA, data, null)
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/Pure/System/session.scala Mon Jan 11 23:00:05 2010 +0100
2.3 @@ -0,0 +1,250 @@
2.4 +/*
2.5 + * Isabelle session, potentially with running prover
2.6 + *
2.7 + * @author Makarius
2.8 + */
2.9 +
2.10 +package isabelle
2.11 +
2.12 +
2.13 +import scala.actors.TIMEOUT
2.14 +import scala.actors.Actor._
2.15 +
2.16 +
2.17 +object Session
2.18 +{
2.19 + /* events */
2.20 +
2.21 + case object Global_Settings
2.22 +
2.23 +
2.24 + /* managed entities */
2.25 +
2.26 + type Entity_ID = String
2.27 +
2.28 + trait Entity
2.29 + {
2.30 + val id: Entity_ID
2.31 + def consume(session: Session, message: XML.Tree): Unit
2.32 + }
2.33 +}
2.34 +
2.35 +
2.36 +class Session(system: Isabelle_System)
2.37 +{
2.38 + /* pervasive event buses */
2.39 +
2.40 + val global_settings = new Event_Bus[Session.Global_Settings.type]
2.41 + val raw_results = new Event_Bus[Isabelle_Process.Result]
2.42 + val results = new Event_Bus[Command]
2.43 +
2.44 + val command_change = new Event_Bus[Command]
2.45 +
2.46 +
2.47 + /* unique ids */
2.48 +
2.49 + private var id_count: BigInt = 0
2.50 + def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
2.51 +
2.52 +
2.53 +
2.54 + /** main actor **/
2.55 +
2.56 + @volatile private var syntax = new Outer_Syntax(system.symbols)
2.57 + def current_syntax: Outer_Syntax = syntax
2.58 +
2.59 + @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
2.60 + def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
2.61 + def lookup_command(id: Session.Entity_ID): Option[Command] =
2.62 + lookup_entity(id) match {
2.63 + case Some(cmd: Command) => Some(cmd)
2.64 + case _ => None
2.65 + }
2.66 +
2.67 + private case class Start(timeout: Int, args: List[String])
2.68 + private case object Stop
2.69 + private case class Begin_Document(path: String)
2.70 +
2.71 + private val session_actor = actor {
2.72 +
2.73 + var prover: Isabelle_Process with Isar_Document = null
2.74 +
2.75 + def register(entity: Session.Entity) { entities += (entity.id -> entity) }
2.76 +
2.77 + var documents = Map[Isar_Document.Document_ID, Document]()
2.78 + def register_document(doc: Document) { documents += (doc.id -> doc) }
2.79 +
2.80 +
2.81 + /* document changes */
2.82 +
2.83 + def handle_change(change: Change)
2.84 + {
2.85 + require(change.parent.isDefined)
2.86 +
2.87 + val (changes, doc) = change.result.join
2.88 + val id_changes = changes map {
2.89 + case (c1, c2) =>
2.90 + (c1.map(_.id).getOrElse(""),
2.91 + c2 match {
2.92 + case None => None
2.93 + case Some(command) =>
2.94 + if (!lookup_command(command.id).isDefined) {
2.95 + register(command)
2.96 + prover.define_command(command.id, system.symbols.encode(command.source))
2.97 + }
2.98 + Some(command.id)
2.99 + })
2.100 + }
2.101 + register_document(doc)
2.102 + prover.edit_document(change.parent.get.id, doc.id, id_changes)
2.103 + }
2.104 +
2.105 +
2.106 + /* prover results */
2.107 +
2.108 + def bad_result(result: Isabelle_Process.Result)
2.109 + {
2.110 + System.err.println("Ignoring prover result: " + result)
2.111 + }
2.112 +
2.113 + def handle_result(result: Isabelle_Process.Result)
2.114 + {
2.115 + raw_results.event(result)
2.116 +
2.117 + val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
2.118 + val target: Option[Session.Entity] =
2.119 + target_id match {
2.120 + case None => None
2.121 + case Some(id) => lookup_entity(id)
2.122 + }
2.123 + if (target.isDefined) target.get.consume(this, result.message)
2.124 + else if (result.kind == Isabelle_Process.Kind.STATUS) {
2.125 + // global status message
2.126 + result.body match {
2.127 +
2.128 + // document state assigment
2.129 + case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
2.130 + documents.get(target_id.get) match {
2.131 + case Some(doc) =>
2.132 + val states =
2.133 + for {
2.134 + XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
2.135 + <- edits
2.136 + cmd <- lookup_command(cmd_id)
2.137 + } yield {
2.138 + val st = cmd.assign_state(state_id)
2.139 + register(st)
2.140 + (cmd, st)
2.141 + }
2.142 + doc.assign_states(states)
2.143 + case None => bad_result(result)
2.144 + }
2.145 +
2.146 + // command and keyword declarations
2.147 + case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
2.148 + syntax += (name, kind)
2.149 + case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
2.150 + syntax += name
2.151 +
2.152 + case _ => if (!result.is_ready) bad_result(result)
2.153 + }
2.154 + }
2.155 + else if (result.kind == Isabelle_Process.Kind.EXIT)
2.156 + prover = null
2.157 + else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw)
2.158 + bad_result(result)
2.159 + }
2.160 +
2.161 +
2.162 + /* prover startup */
2.163 +
2.164 + def startup_error(): String =
2.165 + {
2.166 + val buf = new StringBuilder
2.167 + while (
2.168 + receiveWithin(0) {
2.169 + case result: Isabelle_Process.Result =>
2.170 + if (result.is_raw) {
2.171 + for (text <- XML.content(result.message))
2.172 + buf.append(text)
2.173 + }
2.174 + true
2.175 + case TIMEOUT => false
2.176 + }) {}
2.177 + buf.toString
2.178 + }
2.179 +
2.180 + def prover_startup(timeout: Int): Option[String] =
2.181 + {
2.182 + receiveWithin(timeout) {
2.183 + case result: Isabelle_Process.Result
2.184 + if result.kind == Isabelle_Process.Kind.INIT =>
2.185 + while (receive {
2.186 + case result: Isabelle_Process.Result =>
2.187 + handle_result(result); !result.is_ready
2.188 + }) {}
2.189 + None
2.190 +
2.191 + case result: Isabelle_Process.Result
2.192 + if result.kind == Isabelle_Process.Kind.EXIT =>
2.193 + Some(startup_error())
2.194 +
2.195 + case TIMEOUT => // FIXME clarify
2.196 + prover.kill; Some(startup_error())
2.197 + }
2.198 + }
2.199 +
2.200 +
2.201 + /* main loop */
2.202 +
2.203 + val xml_cache = new XML.Cache(131071)
2.204 +
2.205 + loop {
2.206 + react {
2.207 + case Start(timeout, args) =>
2.208 + if (prover == null) {
2.209 + prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
2.210 + val origin = sender
2.211 + val opt_err = prover_startup(timeout)
2.212 + if (opt_err.isDefined) prover = null
2.213 + origin ! opt_err
2.214 + }
2.215 + else reply(None)
2.216 +
2.217 + case Stop => // FIXME clarify; synchronous
2.218 + if (prover != null) {
2.219 + prover.kill
2.220 + prover = null
2.221 + }
2.222 +
2.223 + case Begin_Document(path: String) if prover != null =>
2.224 + val id = create_id()
2.225 + val doc = Document.empty(id)
2.226 + register_document(doc)
2.227 + prover.begin_document(id, path)
2.228 + reply(doc)
2.229 +
2.230 + case change: Change if prover != null =>
2.231 + handle_change(change)
2.232 +
2.233 + case result: Isabelle_Process.Result =>
2.234 + handle_result(result.cache(xml_cache))
2.235 +
2.236 + case bad if prover != null =>
2.237 + System.err.println("session_actor: ignoring bad message " + bad)
2.238 + }
2.239 + }
2.240 + }
2.241 +
2.242 +
2.243 + /* main methods */
2.244 +
2.245 + def start(timeout: Int, args: List[String]): Option[String] =
2.246 + (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
2.247 +
2.248 + def stop() { session_actor ! Stop }
2.249 + def input(change: Change) { session_actor ! change }
2.250 +
2.251 + def begin_document(path: String): Document =
2.252 + (session_actor !? Begin_Document(path)).asInstanceOf[Document]
2.253 +}
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Pure/Thy/change.scala Mon Jan 11 23:00:05 2010 +0100
3.3 @@ -0,0 +1,42 @@
3.4 +/*
3.5 + * Changes of plain text
3.6 + *
3.7 + * @author Fabian Immler, TU Munich
3.8 + * @author Makarius
3.9 + */
3.10 +
3.11 +package isabelle
3.12 +
3.13 +
3.14 +class Change(
3.15 + val id: Isar_Document.Document_ID,
3.16 + val parent: Option[Change],
3.17 + val edits: List[Text_Edit],
3.18 + val result: Future[(List[Document.Edit], Document)])
3.19 +{
3.20 + def ancestors: Iterator[Change] = new Iterator[Change]
3.21 + {
3.22 + private var state: Option[Change] = Some(Change.this)
3.23 + def hasNext = state.isDefined
3.24 + def next =
3.25 + state match {
3.26 + case Some(change) => state = change.parent; change
3.27 + case None => throw new NoSuchElementException("next on empty iterator")
3.28 + }
3.29 + }
3.30 +
3.31 + def join_document: Document = result.join._2
3.32 + def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
3.33 +
3.34 + def edit(session: Session, edits: List[Text_Edit]): Change =
3.35 + {
3.36 + val new_id = session.create_id()
3.37 + val result: Future[(List[Document.Edit], Document)] =
3.38 + Future.fork {
3.39 + val old_doc = join_document
3.40 + old_doc.await_assignment
3.41 + Document.text_edits(session, old_doc, new_id, edits)
3.42 + }
3.43 + new Change(new_id, Some(this), edits, result)
3.44 + }
3.45 +}
3.46 \ No newline at end of file
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/Thy/command.scala Mon Jan 11 23:00:05 2010 +0100
4.3 @@ -0,0 +1,100 @@
4.4 +/*
4.5 + * Prover commands with semantic state
4.6 + *
4.7 + * @author Johannes Hölzl, TU Munich
4.8 + * @author Fabian Immler, TU Munich
4.9 + */
4.10 +
4.11 +package isabelle
4.12 +
4.13 +
4.14 +import scala.actors.Actor, Actor._
4.15 +import scala.collection.mutable
4.16 +
4.17 +
4.18 +object Command
4.19 +{
4.20 + object Status extends Enumeration
4.21 + {
4.22 + val UNPROCESSED = Value("UNPROCESSED")
4.23 + val FINISHED = Value("FINISHED")
4.24 + val FAILED = Value("FAILED")
4.25 + }
4.26 +
4.27 + case class HighlightInfo(highlight: String) { override def toString = highlight }
4.28 + case class TypeInfo(ty: String)
4.29 + case class RefInfo(file: Option[String], line: Option[Int],
4.30 + command_id: Option[String], offset: Option[Int])
4.31 +}
4.32 +
4.33 +
4.34 +class Command(
4.35 + val id: Isar_Document.Command_ID,
4.36 + val span: Thy_Syntax.Span)
4.37 + extends Session.Entity
4.38 +{
4.39 + /* classification */
4.40 +
4.41 + def is_command: Boolean = !span.isEmpty && span.first.is_command
4.42 + def is_ignored: Boolean = span.forall(_.is_ignored)
4.43 + def is_malformed: Boolean = !is_command && !is_ignored
4.44 +
4.45 + def name: String = if (is_command) span.first.content else ""
4.46 + override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
4.47 +
4.48 +
4.49 + /* source text */
4.50 +
4.51 + val source: String = span.map(_.source).mkString
4.52 + def source(i: Int, j: Int): String = source.substring(i, j)
4.53 + def length: Int = source.length
4.54 +
4.55 + lazy val symbol_index = new Symbol.Index(source)
4.56 +
4.57 +
4.58 + /* accumulated messages */
4.59 +
4.60 + @volatile protected var state = new State(this)
4.61 + def current_state: State = state
4.62 +
4.63 + private case class Consume(session: Session, message: XML.Tree)
4.64 + private case object Assign
4.65 +
4.66 + private val accumulator = actor {
4.67 + var assigned = false
4.68 + loop {
4.69 + react {
4.70 + case Consume(session: Session, message: XML.Tree) if !assigned =>
4.71 + state = state.+(session, message)
4.72 +
4.73 + case Assign =>
4.74 + assigned = true // single assignment
4.75 + reply(())
4.76 +
4.77 + case bad => System.err.println("command accumulator: ignoring bad message " + bad)
4.78 + }
4.79 + }
4.80 + }
4.81 +
4.82 + def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
4.83 +
4.84 + def assign_state(state_id: Isar_Document.State_ID): Command =
4.85 + {
4.86 + val cmd = new Command(state_id, span)
4.87 + accumulator !? Assign
4.88 + cmd.state = current_state
4.89 + cmd
4.90 + }
4.91 +
4.92 +
4.93 + /* markup */
4.94 +
4.95 + lazy val empty_markup = new Markup_Text(Nil, source)
4.96 +
4.97 + def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
4.98 + {
4.99 + val start = symbol_index.decode(begin)
4.100 + val stop = symbol_index.decode(end)
4.101 + new Markup_Tree(new Markup_Node(start, stop, info), Nil)
4.102 + }
4.103 +}
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Pure/Thy/document.scala Mon Jan 11 23:00:05 2010 +0100
5.3 @@ -0,0 +1,197 @@
5.4 +/*
5.5 + * Document as editable list of commands
5.6 + *
5.7 + * @author Makarius
5.8 + */
5.9 +
5.10 +package isabelle
5.11 +
5.12 +
5.13 +object Document
5.14 +{
5.15 + /* command start positions */
5.16 +
5.17 + def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
5.18 + {
5.19 + var offset = 0
5.20 + for (cmd <- commands.elements) yield {
5.21 + val start = offset
5.22 + offset += cmd.length
5.23 + (cmd, start)
5.24 + }
5.25 + }
5.26 +
5.27 +
5.28 + /* empty document */
5.29 +
5.30 + def empty(id: Isar_Document.Document_ID): Document =
5.31 + {
5.32 + val doc = new Document(id, Linear_Set(), Map())
5.33 + doc.assign_states(Nil)
5.34 + doc
5.35 + }
5.36 +
5.37 +
5.38 + // FIXME
5.39 + var phase0: List[Text_Edit] = null
5.40 + var phase1: Linear_Set[Command] = null
5.41 + var phase2: Linear_Set[Command] = null
5.42 + var phase3: List[Edit] = null
5.43 +
5.44 +
5.45 +
5.46 + /** document edits **/
5.47 +
5.48 + type Edit = (Option[Command], Option[Command])
5.49 +
5.50 + def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
5.51 + edits: List[Text_Edit]): (List[Edit], Document) =
5.52 + {
5.53 + require(old_doc.assignment.is_finished)
5.54 +
5.55 +
5.56 + /* unparsed dummy commands */
5.57 +
5.58 + def unparsed(source: String) =
5.59 + new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
5.60 +
5.61 + def is_unparsed(command: Command) = command.id == null
5.62 +
5.63 + assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
5.64 +
5.65 +
5.66 + /* phase 1: edit individual command source */
5.67 +
5.68 + def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
5.69 + {
5.70 + eds match {
5.71 + case e :: es =>
5.72 + command_starts(commands).find { // FIXME relative search!
5.73 + case (cmd, cmd_start) =>
5.74 + e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
5.75 + } match {
5.76 + case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
5.77 + val (rest, text) = e.edit(cmd.source, cmd_start)
5.78 + val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
5.79 + edit_text(rest.toList ::: es, new_commands)
5.80 +
5.81 + case Some((cmd, cmd_start)) =>
5.82 + edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
5.83 +
5.84 + case None =>
5.85 + require(e.is_insert && e.start == 0)
5.86 + edit_text(es, commands.insert_after(None, unparsed(e.text)))
5.87 + }
5.88 + case Nil => commands
5.89 + }
5.90 + }
5.91 +
5.92 +
5.93 + /* phase 2: recover command spans */
5.94 +
5.95 + def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
5.96 + {
5.97 + // FIXME relative search!
5.98 + commands.elements.find(is_unparsed) match {
5.99 + case Some(first_unparsed) =>
5.100 + val prefix = commands.prev(first_unparsed)
5.101 + val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
5.102 + val suffix = commands.next(body.last)
5.103 +
5.104 + val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
5.105 + val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
5.106 +
5.107 + val (before_edit, spans1) =
5.108 + if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
5.109 + (prefix, spans0.tail)
5.110 + else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
5.111 +
5.112 + val (after_edit, spans2) =
5.113 + if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
5.114 + (suffix, spans1.take(spans1.length - 1))
5.115 + else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
5.116 +
5.117 + val inserted = spans2.map(span => new Command(session.create_id(), span))
5.118 + val new_commands =
5.119 + commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
5.120 + parse_spans(new_commands)
5.121 +
5.122 + case None => commands
5.123 + }
5.124 + }
5.125 +
5.126 +
5.127 + /* phase 3: resulting document edits */
5.128 +
5.129 + val result = Library.timeit("text_edits") {
5.130 + val commands0 = old_doc.commands
5.131 + val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
5.132 + val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
5.133 +
5.134 + val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
5.135 + val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
5.136 +
5.137 + val doc_edits =
5.138 + removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
5.139 + inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
5.140 +
5.141 + val former_states = old_doc.assignment.join -- removed_commands
5.142 +
5.143 + phase0 = edits
5.144 + phase1 = commands1
5.145 + phase2 = commands2
5.146 + phase3 = doc_edits
5.147 +
5.148 + (doc_edits, new Document(new_id, commands2, former_states))
5.149 + }
5.150 + result
5.151 + }
5.152 +}
5.153 +
5.154 +
5.155 +class Document(
5.156 + val id: Isar_Document.Document_ID,
5.157 + val commands: Linear_Set[Command],
5.158 + former_states: Map[Command, Command])
5.159 +{
5.160 + /* command ranges */
5.161 +
5.162 + def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
5.163 +
5.164 + def command_start(cmd: Command): Option[Int] =
5.165 + command_starts.find(_._1 == cmd).map(_._2)
5.166 +
5.167 + def command_range(i: Int): Iterator[(Command, Int)] =
5.168 + command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
5.169 +
5.170 + def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
5.171 + command_range(i) takeWhile { case (_, start) => start < j }
5.172 +
5.173 + def command_at(i: Int): Option[(Command, Int)] =
5.174 + {
5.175 + val range = command_range(i)
5.176 + if (range.hasNext) Some(range.next) else None
5.177 + }
5.178 +
5.179 +
5.180 + /* command state assignment */
5.181 +
5.182 + val assignment = Future.promise[Map[Command, Command]]
5.183 + def await_assignment { assignment.join }
5.184 +
5.185 + @volatile private var tmp_states = former_states
5.186 + private val time0 = System.currentTimeMillis
5.187 +
5.188 + def assign_states(new_states: List[(Command, Command)])
5.189 + {
5.190 + assignment.fulfill(tmp_states ++ new_states)
5.191 + tmp_states = Map()
5.192 + System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
5.193 + }
5.194 +
5.195 + def current_state(cmd: Command): Option[State] =
5.196 + {
5.197 + require(assignment.is_finished)
5.198 + (assignment.join).get(cmd).map(_.current_state)
5.199 + }
5.200 +}
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Pure/Thy/markup_node.scala Mon Jan 11 23:00:05 2010 +0100
6.3 @@ -0,0 +1,111 @@
6.4 +/*
6.5 + * Document markup nodes, with connection to Swing tree model
6.6 + *
6.7 + * @author Fabian Immler, TU Munich
6.8 + * @author Makarius
6.9 + */
6.10 +
6.11 +package isabelle
6.12 +
6.13 +
6.14 +import javax.swing.tree.DefaultMutableTreeNode
6.15 +
6.16 +
6.17 +
6.18 +class Markup_Node(val start: Int, val stop: Int, val info: Any)
6.19 +{
6.20 + def fits_into(that: Markup_Node): Boolean =
6.21 + that.start <= this.start && this.stop <= that.stop
6.22 +}
6.23 +
6.24 +
6.25 +class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
6.26 +{
6.27 + def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
6.28 +
6.29 + private def add(branch: Markup_Tree) = // FIXME avoid sort
6.30 + set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
6.31 +
6.32 + private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
6.33 +
6.34 + def + (new_tree: Markup_Tree): Markup_Tree =
6.35 + {
6.36 + val new_node = new_tree.node
6.37 + if (new_node fits_into node) {
6.38 + var inserted = false
6.39 + val new_branches =
6.40 + branches.map(branch =>
6.41 + if ((new_node fits_into branch.node) && !inserted) {
6.42 + inserted = true
6.43 + branch + new_tree
6.44 + }
6.45 + else branch)
6.46 + if (!inserted) {
6.47 + // new_tree did not fit into children of this
6.48 + // -> insert between this and its branches
6.49 + val fitting = branches filter(_.node fits_into new_node)
6.50 + (this remove fitting) add ((new_tree /: fitting)(_ + _))
6.51 + }
6.52 + else set_branches(new_branches)
6.53 + }
6.54 + else {
6.55 + System.err.println("ignored nonfitting markup: " + new_node)
6.56 + this
6.57 + }
6.58 + }
6.59 +
6.60 + def flatten: List[Markup_Node] =
6.61 + {
6.62 + var next_x = node.start
6.63 + if (branches.isEmpty) List(this.node)
6.64 + else {
6.65 + val filled_gaps =
6.66 + for {
6.67 + child <- branches
6.68 + markups =
6.69 + if (next_x < child.node.start)
6.70 + new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
6.71 + else child.flatten
6.72 + update = (next_x = child.node.stop)
6.73 + markup <- markups
6.74 + } yield markup
6.75 + if (next_x < node.stop)
6.76 + filled_gaps + new Markup_Node(next_x, node.stop, node.info)
6.77 + else filled_gaps
6.78 + }
6.79 + }
6.80 +}
6.81 +
6.82 +
6.83 +class Markup_Text(val markup: List[Markup_Tree], val content: String)
6.84 +{
6.85 + private lazy val root =
6.86 + new Markup_Tree(new Markup_Node(0, content.length, None), markup)
6.87 +
6.88 + def + (new_tree: Markup_Tree): Markup_Text =
6.89 + new Markup_Text((root + new_tree).branches, content)
6.90 +
6.91 + def filter(pred: Markup_Node => Boolean): Markup_Text =
6.92 + {
6.93 + def filt(tree: Markup_Tree): List[Markup_Tree] =
6.94 + {
6.95 + val branches = tree.branches.flatMap(filt(_))
6.96 + if (pred(tree.node)) List(tree.set_branches(branches))
6.97 + else branches
6.98 + }
6.99 + new Markup_Text(markup.flatMap(filt(_)), content)
6.100 + }
6.101 +
6.102 + def flatten: List[Markup_Node] = markup.flatten(_.flatten)
6.103 +
6.104 + def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
6.105 + {
6.106 + def swing(tree: Markup_Tree): DefaultMutableTreeNode =
6.107 + {
6.108 + val node = swing_node(tree.node)
6.109 + tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
6.110 + node
6.111 + }
6.112 + swing(root)
6.113 + }
6.114 +}
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/Pure/Thy/state.scala Mon Jan 11 23:00:05 2010 +0100
7.3 @@ -0,0 +1,117 @@
7.4 +/*
7.5 + * Accumulating results from prover
7.6 + *
7.7 + * @author Fabian Immler, TU Munich
7.8 + * @author Makarius
7.9 + */
7.10 +
7.11 +package isabelle
7.12 +
7.13 +
7.14 +class State(
7.15 + val command: Command,
7.16 + val status: Command.Status.Value,
7.17 + val rev_results: List[XML.Tree],
7.18 + val markup_root: Markup_Text)
7.19 +{
7.20 + def this(command: Command) =
7.21 + this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
7.22 +
7.23 +
7.24 + /* content */
7.25 +
7.26 + private def set_status(st: Command.Status.Value): State =
7.27 + new State(command, st, rev_results, markup_root)
7.28 +
7.29 + private def add_result(res: XML.Tree): State =
7.30 + new State(command, status, res :: rev_results, markup_root)
7.31 +
7.32 + private def add_markup(node: Markup_Tree): State =
7.33 + new State(command, status, rev_results, markup_root + node)
7.34 +
7.35 + lazy val results = rev_results.reverse
7.36 +
7.37 +
7.38 + /* markup */
7.39 +
7.40 + lazy val highlight: Markup_Text =
7.41 + {
7.42 + markup_root.filter(_.info match {
7.43 + case Command.HighlightInfo(_) => true
7.44 + case _ => false
7.45 + })
7.46 + }
7.47 +
7.48 + private lazy val types: List[Markup_Node] =
7.49 + markup_root.filter(_.info match {
7.50 + case Command.TypeInfo(_) => true
7.51 + case _ => false }).flatten
7.52 +
7.53 + def type_at(pos: Int): Option[String] =
7.54 + {
7.55 + types.find(t => t.start <= pos && pos < t.stop) match {
7.56 + case Some(t) =>
7.57 + t.info match {
7.58 + case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
7.59 + case _ => None
7.60 + }
7.61 + case None => None
7.62 + }
7.63 + }
7.64 +
7.65 + private lazy val refs: List[Markup_Node] =
7.66 + markup_root.filter(_.info match {
7.67 + case Command.RefInfo(_, _, _, _) => true
7.68 + case _ => false }).flatten
7.69 +
7.70 + def ref_at(pos: Int): Option[Markup_Node] =
7.71 + refs.find(t => t.start <= pos && pos < t.stop)
7.72 +
7.73 +
7.74 + /* message dispatch */
7.75 +
7.76 + def + (session: Session, message: XML.Tree): State =
7.77 + {
7.78 + val changed: State =
7.79 + message match {
7.80 + case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
7.81 + (this /: elems)((state, elem) =>
7.82 + elem match {
7.83 + case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
7.84 + case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
7.85 + case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
7.86 + case XML.Elem(kind, atts, body) =>
7.87 + val (begin, end) = Position.get_offsets(atts)
7.88 + if (begin.isEmpty || end.isEmpty) state
7.89 + else if (kind == Markup.ML_TYPING) {
7.90 + val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
7.91 + state.add_markup(
7.92 + command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
7.93 + }
7.94 + else if (kind == Markup.ML_REF) {
7.95 + body match {
7.96 + case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
7.97 + state.add_markup(command.markup_node(
7.98 + begin.get - 1, end.get - 1,
7.99 + Command.RefInfo(
7.100 + Position.get_file(atts),
7.101 + Position.get_line(atts),
7.102 + Position.get_id(atts),
7.103 + Position.get_offset(atts))))
7.104 + case _ => state
7.105 + }
7.106 + }
7.107 + else {
7.108 + state.add_markup(
7.109 + command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
7.110 + }
7.111 + case _ =>
7.112 + System.err.println("ignored status report: " + elem)
7.113 + state
7.114 + })
7.115 + case _ => add_result(message)
7.116 + }
7.117 + if (!(this eq changed)) session.command_change.event(command)
7.118 + changed
7.119 + }
7.120 +}
8.1 --- a/src/Pure/build-jars Mon Jan 11 22:44:21 2010 +0100
8.2 +++ b/src/Pure/build-jars Mon Jan 11 23:00:05 2010 +0100
8.3 @@ -45,10 +45,16 @@
8.4 System/isabelle_syntax.scala
8.5 System/isabelle_system.scala
8.6 System/platform.scala
8.7 + System/session.scala
8.8 System/session_manager.scala
8.9 System/standard_system.scala
8.10 + Thy/change.scala
8.11 + Thy/command.scala
8.12 Thy/completion.scala
8.13 + Thy/document.scala
8.14 Thy/html.scala
8.15 + Thy/markup_node.scala
8.16 + Thy/state.scala
8.17 Thy/text_edit.scala
8.18 Thy/thy_header.scala
8.19 Thy/thy_syntax.scala
9.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 11 22:44:21 2010 +0100
9.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Jan 11 23:00:05 2010 +0100
9.3 @@ -8,8 +8,6 @@
9.4 package isabelle.jedit
9.5
9.6
9.7 -import isabelle.proofdocument.{Change, Command, Document, Session}
9.8 -
9.9 import scala.actors.Actor, Actor._
9.10 import scala.collection.mutable
9.11
10.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 22:44:21 2010 +0100
10.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Mon Jan 11 23:00:05 2010 +0100
10.3 @@ -8,8 +8,6 @@
10.4 package isabelle.jedit
10.5
10.6
10.7 -import isabelle.proofdocument.{Command, Document, Session}
10.8 -
10.9 import scala.actors.Actor._
10.10
10.11 import java.awt.event.{MouseAdapter, MouseEvent}
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Mon Jan 11 23:00:05 2010 +0100
11.3 @@ -0,0 +1,140 @@
11.4 +/*
11.5 + * HTML panel based on Lobo/Cobra
11.6 + *
11.7 + * @author Makarius
11.8 + */
11.9 +
11.10 +package isabelle.jedit
11.11 +
11.12 +
11.13 +import java.io.StringReader
11.14 +import java.awt.{BorderLayout, Dimension}
11.15 +import java.awt.event.MouseEvent
11.16 +
11.17 +import javax.swing.{JButton, JPanel, JScrollPane}
11.18 +import java.util.logging.{Logger, Level}
11.19 +
11.20 +import org.w3c.dom.html2.HTMLElement
11.21 +
11.22 +import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
11.23 +import org.lobobrowser.html.gui.HtmlPanel
11.24 +import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
11.25 +import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
11.26 +
11.27 +import scala.io.Source
11.28 +import scala.actors.Actor._
11.29 +
11.30 +
11.31 +object HTML_Panel
11.32 +{
11.33 + sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
11.34 + case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
11.35 + case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
11.36 + case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
11.37 + case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
11.38 + case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
11.39 +}
11.40 +
11.41 +
11.42 +class HTML_Panel(
11.43 + sys: Isabelle_System,
11.44 + initial_font_size: Int,
11.45 + handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
11.46 +{
11.47 + // global logging
11.48 + Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
11.49 +
11.50 +
11.51 + /* document template */
11.52 +
11.53 + private def try_file(name: String): String =
11.54 + {
11.55 + val file = sys.platform_file(name)
11.56 + if (file.isFile) Source.fromFile(file).mkString else ""
11.57 + }
11.58 +
11.59 + private def template(font_size: Int): String =
11.60 + """<?xml version="1.0" encoding="utf-8"?>
11.61 +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
11.62 + "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
11.63 +<html xmlns="http://www.w3.org/1999/xhtml">
11.64 +<head>
11.65 +<style media="all" type="text/css">
11.66 +""" +
11.67 + try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
11.68 + try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
11.69 + "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
11.70 +"""
11.71 +</style>
11.72 +</head>
11.73 +<body/>
11.74 +</html>
11.75 +"""
11.76 +
11.77 +
11.78 + /* actor with local state */
11.79 +
11.80 + private val ucontext = new SimpleUserAgentContext
11.81 +
11.82 + private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
11.83 + {
11.84 + private def handle(event: HTML_Panel.Event): Boolean =
11.85 + if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
11.86 + else false
11.87 +
11.88 + override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
11.89 + handle(HTML_Panel.Context_Menu(elem, event))
11.90 + override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
11.91 + handle(HTML_Panel.Mouse_Click(elem, event))
11.92 + override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
11.93 + handle(HTML_Panel.Double_Click(elem, event))
11.94 + override def onMouseOver(elem: HTMLElement, event: MouseEvent)
11.95 + { handle(HTML_Panel.Mouse_Over(elem, event)) }
11.96 + override def onMouseOut(elem: HTMLElement, event: MouseEvent)
11.97 + { handle(HTML_Panel.Mouse_Out(elem, event)) }
11.98 + }
11.99 +
11.100 + private val builder = new DocumentBuilderImpl(ucontext, rcontext)
11.101 +
11.102 + private case class Init(font_size: Int)
11.103 + private case class Render(body: List[XML.Tree])
11.104 +
11.105 + private val main_actor = actor {
11.106 + // crude double buffering
11.107 + var doc1: org.w3c.dom.Document = null
11.108 + var doc2: org.w3c.dom.Document = null
11.109 +
11.110 + loop {
11.111 + react {
11.112 + case Init(font_size) =>
11.113 + val src = template(font_size)
11.114 + def parse() =
11.115 + builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
11.116 + doc1 = parse()
11.117 + doc2 = parse()
11.118 + Swing_Thread.now { setDocument(doc1, rcontext) }
11.119 +
11.120 + case Render(body) =>
11.121 + val doc = doc2
11.122 + val node =
11.123 + XML.document_node(doc,
11.124 + XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
11.125 + doc.removeChild(doc.getLastChild())
11.126 + doc.appendChild(node)
11.127 + doc2 = doc1
11.128 + doc1 = doc
11.129 + Swing_Thread.now { setDocument(doc1, rcontext) }
11.130 +
11.131 + case bad => System.err.println("main_actor: ignoring bad message " + bad)
11.132 + }
11.133 + }
11.134 + }
11.135 +
11.136 + main_actor ! Init(initial_font_size)
11.137 +
11.138 +
11.139 + /* main method wrappers */
11.140 +
11.141 + def init(font_size: Int) { main_actor ! Init(font_size) }
11.142 + def render(body: List[XML.Tree]) { main_actor ! Render(body) }
11.143 +}
12.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 22:44:21 2010 +0100
12.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Mon Jan 11 23:00:05 2010 +0100
12.3 @@ -6,7 +6,6 @@
12.4
12.5 package isabelle.jedit
12.6
12.7 -import isabelle.proofdocument.Command
12.8
12.9 import java.io.File
12.10
13.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 22:44:21 2010 +0100
13.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon Jan 11 23:00:05 2010 +0100
13.3 @@ -19,8 +19,6 @@
13.4 import errorlist.DefaultErrorSource
13.5 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
13.6
13.7 -import isabelle.proofdocument.{Command, Markup_Node, Document}
13.8 -
13.9
13.10 class Isabelle_Sidekick extends SideKickParser("isabelle")
13.11 {
14.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 22:44:21 2010 +0100
14.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jan 11 23:00:05 2010 +0100
14.3 @@ -7,8 +7,6 @@
14.4 package isabelle.jedit
14.5
14.6
14.7 -import isabelle.proofdocument.{Command, HTML_Panel, Session}
14.8 -
14.9 import scala.actors.Actor._
14.10
14.11 import javax.swing.JPanel
15.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala Mon Jan 11 22:44:21 2010 +0100
15.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala Mon Jan 11 23:00:05 2010 +0100
15.3 @@ -9,8 +9,6 @@
15.4 package isabelle.jedit
15.5
15.6
15.7 -import isabelle.proofdocument.Session
15.8 -
15.9 import java.io.{FileInputStream, IOException}
15.10 import java.awt.Font
15.11 import javax.swing.JTextArea
16.1 --- a/src/Tools/jEdit/src/proofdocument/change.scala Mon Jan 11 22:44:21 2010 +0100
16.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
16.3 @@ -1,42 +0,0 @@
16.4 -/*
16.5 - * Changes of plain text
16.6 - *
16.7 - * @author Fabian Immler, TU Munich
16.8 - * @author Makarius
16.9 - */
16.10 -
16.11 -package isabelle.proofdocument
16.12 -
16.13 -
16.14 -class Change(
16.15 - val id: Isar_Document.Document_ID,
16.16 - val parent: Option[Change],
16.17 - val edits: List[Text_Edit],
16.18 - val result: Future[(List[Document.Edit], Document)])
16.19 -{
16.20 - def ancestors: Iterator[Change] = new Iterator[Change]
16.21 - {
16.22 - private var state: Option[Change] = Some(Change.this)
16.23 - def hasNext = state.isDefined
16.24 - def next =
16.25 - state match {
16.26 - case Some(change) => state = change.parent; change
16.27 - case None => throw new NoSuchElementException("next on empty iterator")
16.28 - }
16.29 - }
16.30 -
16.31 - def join_document: Document = result.join._2
16.32 - def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
16.33 -
16.34 - def edit(session: Session, edits: List[Text_Edit]): Change =
16.35 - {
16.36 - val new_id = session.create_id()
16.37 - val result: Future[(List[Document.Edit], Document)] =
16.38 - Future.fork {
16.39 - val old_doc = join_document
16.40 - old_doc.await_assignment
16.41 - Document.text_edits(session, old_doc, new_id, edits)
16.42 - }
16.43 - new Change(new_id, Some(this), edits, result)
16.44 - }
16.45 -}
16.46 \ No newline at end of file
17.1 --- a/src/Tools/jEdit/src/proofdocument/command.scala Mon Jan 11 22:44:21 2010 +0100
17.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
17.3 @@ -1,102 +0,0 @@
17.4 -/*
17.5 - * Prover commands with semantic state
17.6 - *
17.7 - * @author Johannes Hölzl, TU Munich
17.8 - * @author Fabian Immler, TU Munich
17.9 - */
17.10 -
17.11 -package isabelle.proofdocument
17.12 -
17.13 -
17.14 -import scala.actors.Actor, Actor._
17.15 -import scala.collection.mutable
17.16 -
17.17 -import isabelle.jedit.Isabelle
17.18 -
17.19 -
17.20 -object Command
17.21 -{
17.22 - object Status extends Enumeration
17.23 - {
17.24 - val UNPROCESSED = Value("UNPROCESSED")
17.25 - val FINISHED = Value("FINISHED")
17.26 - val FAILED = Value("FAILED")
17.27 - }
17.28 -
17.29 - case class HighlightInfo(highlight: String) { override def toString = highlight }
17.30 - case class TypeInfo(ty: String)
17.31 - case class RefInfo(file: Option[String], line: Option[Int],
17.32 - command_id: Option[String], offset: Option[Int])
17.33 -}
17.34 -
17.35 -
17.36 -class Command(
17.37 - val id: Isar_Document.Command_ID,
17.38 - val span: Thy_Syntax.Span)
17.39 - extends Session.Entity
17.40 -{
17.41 - /* classification */
17.42 -
17.43 - def is_command: Boolean = !span.isEmpty && span.first.is_command
17.44 - def is_ignored: Boolean = span.forall(_.is_ignored)
17.45 - def is_malformed: Boolean = !is_command && !is_ignored
17.46 -
17.47 - def name: String = if (is_command) span.first.content else ""
17.48 - override def toString = if (is_command) name else if (is_ignored) "<ignored>" else "<malformed>"
17.49 -
17.50 -
17.51 - /* source text */
17.52 -
17.53 - val source: String = span.map(_.source).mkString
17.54 - def source(i: Int, j: Int): String = source.substring(i, j)
17.55 - def length: Int = source.length
17.56 -
17.57 - lazy val symbol_index = new Symbol.Index(source)
17.58 -
17.59 -
17.60 - /* accumulated messages */
17.61 -
17.62 - @volatile protected var state = new State(this)
17.63 - def current_state: State = state
17.64 -
17.65 - private case class Consume(session: Session, message: XML.Tree)
17.66 - private case object Assign
17.67 -
17.68 - private val accumulator = actor {
17.69 - var assigned = false
17.70 - loop {
17.71 - react {
17.72 - case Consume(session: Session, message: XML.Tree) if !assigned =>
17.73 - state = state.+(session, message)
17.74 -
17.75 - case Assign =>
17.76 - assigned = true // single assignment
17.77 - reply(())
17.78 -
17.79 - case bad => System.err.println("command accumulator: ignoring bad message " + bad)
17.80 - }
17.81 - }
17.82 - }
17.83 -
17.84 - def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
17.85 -
17.86 - def assign_state(state_id: Isar_Document.State_ID): Command =
17.87 - {
17.88 - val cmd = new Command(state_id, span)
17.89 - accumulator !? Assign
17.90 - cmd.state = current_state
17.91 - cmd
17.92 - }
17.93 -
17.94 -
17.95 - /* markup */
17.96 -
17.97 - lazy val empty_markup = new Markup_Text(Nil, source)
17.98 -
17.99 - def markup_node(begin: Int, end: Int, info: Any): Markup_Tree =
17.100 - {
17.101 - val start = symbol_index.decode(begin)
17.102 - val stop = symbol_index.decode(end)
17.103 - new Markup_Tree(new Markup_Node(start, stop, info), Nil)
17.104 - }
17.105 -}
18.1 --- a/src/Tools/jEdit/src/proofdocument/document.scala Mon Jan 11 22:44:21 2010 +0100
18.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
18.3 @@ -1,197 +0,0 @@
18.4 -/*
18.5 - * Document as editable list of commands
18.6 - *
18.7 - * @author Makarius
18.8 - */
18.9 -
18.10 -package isabelle.proofdocument
18.11 -
18.12 -
18.13 -object Document
18.14 -{
18.15 - /* command start positions */
18.16 -
18.17 - def command_starts(commands: Linear_Set[Command]): Iterator[(Command, Int)] =
18.18 - {
18.19 - var offset = 0
18.20 - for (cmd <- commands.elements) yield {
18.21 - val start = offset
18.22 - offset += cmd.length
18.23 - (cmd, start)
18.24 - }
18.25 - }
18.26 -
18.27 -
18.28 - /* empty document */
18.29 -
18.30 - def empty(id: Isar_Document.Document_ID): Document =
18.31 - {
18.32 - val doc = new Document(id, Linear_Set(), Map())
18.33 - doc.assign_states(Nil)
18.34 - doc
18.35 - }
18.36 -
18.37 -
18.38 - // FIXME
18.39 - var phase0: List[Text_Edit] = null
18.40 - var phase1: Linear_Set[Command] = null
18.41 - var phase2: Linear_Set[Command] = null
18.42 - var phase3: List[Edit] = null
18.43 -
18.44 -
18.45 -
18.46 - /** document edits **/
18.47 -
18.48 - type Edit = (Option[Command], Option[Command])
18.49 -
18.50 - def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
18.51 - edits: List[Text_Edit]): (List[Edit], Document) =
18.52 - {
18.53 - require(old_doc.assignment.is_finished)
18.54 -
18.55 -
18.56 - /* unparsed dummy commands */
18.57 -
18.58 - def unparsed(source: String) =
18.59 - new Command(null, List(Outer_Lex.Token(Outer_Lex.Token_Kind.UNPARSED, source)))
18.60 -
18.61 - def is_unparsed(command: Command) = command.id == null
18.62 -
18.63 - assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
18.64 -
18.65 -
18.66 - /* phase 1: edit individual command source */
18.67 -
18.68 - def edit_text(eds: List[Text_Edit], commands: Linear_Set[Command]): Linear_Set[Command] =
18.69 - {
18.70 - eds match {
18.71 - case e :: es =>
18.72 - command_starts(commands).find { // FIXME relative search!
18.73 - case (cmd, cmd_start) =>
18.74 - e.can_edit(cmd.source, cmd_start) || e.is_insert && e.start == cmd_start + cmd.length
18.75 - } match {
18.76 - case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
18.77 - val (rest, text) = e.edit(cmd.source, cmd_start)
18.78 - val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
18.79 - edit_text(rest.toList ::: es, new_commands)
18.80 -
18.81 - case Some((cmd, cmd_start)) =>
18.82 - edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
18.83 -
18.84 - case None =>
18.85 - require(e.is_insert && e.start == 0)
18.86 - edit_text(es, commands.insert_after(None, unparsed(e.text)))
18.87 - }
18.88 - case Nil => commands
18.89 - }
18.90 - }
18.91 -
18.92 -
18.93 - /* phase 2: recover command spans */
18.94 -
18.95 - def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
18.96 - {
18.97 - // FIXME relative search!
18.98 - commands.elements.find(is_unparsed) match {
18.99 - case Some(first_unparsed) =>
18.100 - val prefix = commands.prev(first_unparsed)
18.101 - val body = commands.elements(first_unparsed).takeWhile(is_unparsed).toList
18.102 - val suffix = commands.next(body.last)
18.103 -
18.104 - val sources = (prefix.toList ::: body ::: suffix.toList).flatMap(_.span.map(_.source))
18.105 - val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
18.106 -
18.107 - val (before_edit, spans1) =
18.108 - if (!spans0.isEmpty && Some(spans0.first) == prefix.map(_.span))
18.109 - (prefix, spans0.tail)
18.110 - else (if (prefix.isDefined) commands.prev(prefix.get) else None, spans0)
18.111 -
18.112 - val (after_edit, spans2) =
18.113 - if (!spans1.isEmpty && Some(spans1.last) == suffix.map(_.span))
18.114 - (suffix, spans1.take(spans1.length - 1))
18.115 - else (if (suffix.isDefined) commands.next(suffix.get) else None, spans1)
18.116 -
18.117 - val inserted = spans2.map(span => new Command(session.create_id(), span))
18.118 - val new_commands =
18.119 - commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
18.120 - parse_spans(new_commands)
18.121 -
18.122 - case None => commands
18.123 - }
18.124 - }
18.125 -
18.126 -
18.127 - /* phase 3: resulting document edits */
18.128 -
18.129 - val result = Library.timeit("text_edits") {
18.130 - val commands0 = old_doc.commands
18.131 - val commands1 = Library.timeit("edit_text") { edit_text(edits, commands0) }
18.132 - val commands2 = Library.timeit("parse_spans") { parse_spans(commands1) }
18.133 -
18.134 - val removed_commands = commands0.elements.filter(!commands2.contains(_)).toList
18.135 - val inserted_commands = commands2.elements.filter(!commands0.contains(_)).toList
18.136 -
18.137 - val doc_edits =
18.138 - removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
18.139 - inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
18.140 -
18.141 - val former_states = old_doc.assignment.join -- removed_commands
18.142 -
18.143 - phase0 = edits
18.144 - phase1 = commands1
18.145 - phase2 = commands2
18.146 - phase3 = doc_edits
18.147 -
18.148 - (doc_edits, new Document(new_id, commands2, former_states))
18.149 - }
18.150 - result
18.151 - }
18.152 -}
18.153 -
18.154 -
18.155 -class Document(
18.156 - val id: Isar_Document.Document_ID,
18.157 - val commands: Linear_Set[Command],
18.158 - former_states: Map[Command, Command])
18.159 -{
18.160 - /* command ranges */
18.161 -
18.162 - def command_starts: Iterator[(Command, Int)] = Document.command_starts(commands)
18.163 -
18.164 - def command_start(cmd: Command): Option[Int] =
18.165 - command_starts.find(_._1 == cmd).map(_._2)
18.166 -
18.167 - def command_range(i: Int): Iterator[(Command, Int)] =
18.168 - command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
18.169 -
18.170 - def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
18.171 - command_range(i) takeWhile { case (_, start) => start < j }
18.172 -
18.173 - def command_at(i: Int): Option[(Command, Int)] =
18.174 - {
18.175 - val range = command_range(i)
18.176 - if (range.hasNext) Some(range.next) else None
18.177 - }
18.178 -
18.179 -
18.180 - /* command state assignment */
18.181 -
18.182 - val assignment = Future.promise[Map[Command, Command]]
18.183 - def await_assignment { assignment.join }
18.184 -
18.185 - @volatile private var tmp_states = former_states
18.186 - private val time0 = System.currentTimeMillis
18.187 -
18.188 - def assign_states(new_states: List[(Command, Command)])
18.189 - {
18.190 - assignment.fulfill(tmp_states ++ new_states)
18.191 - tmp_states = Map()
18.192 - System.err.println("assign_states: " + (System.currentTimeMillis - time0) + " ms elapsed time")
18.193 - }
18.194 -
18.195 - def current_state(cmd: Command): Option[State] =
18.196 - {
18.197 - require(assignment.is_finished)
18.198 - (assignment.join).get(cmd).map(_.current_state)
18.199 - }
18.200 -}
19.1 --- a/src/Tools/jEdit/src/proofdocument/html_panel.scala Mon Jan 11 22:44:21 2010 +0100
19.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
19.3 @@ -1,140 +0,0 @@
19.4 -/*
19.5 - * HTML panel based on Lobo/Cobra
19.6 - *
19.7 - * @author Makarius
19.8 - */
19.9 -
19.10 -package isabelle.proofdocument
19.11 -
19.12 -
19.13 -import java.io.StringReader
19.14 -import java.awt.{BorderLayout, Dimension}
19.15 -import java.awt.event.MouseEvent
19.16 -
19.17 -import javax.swing.{JButton, JPanel, JScrollPane}
19.18 -import java.util.logging.{Logger, Level}
19.19 -
19.20 -import org.w3c.dom.html2.HTMLElement
19.21 -
19.22 -import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
19.23 -import org.lobobrowser.html.gui.HtmlPanel
19.24 -import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
19.25 -import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
19.26 -
19.27 -import scala.io.Source
19.28 -import scala.actors.Actor._
19.29 -
19.30 -
19.31 -object HTML_Panel
19.32 -{
19.33 - sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
19.34 - case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
19.35 - case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
19.36 - case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
19.37 - case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
19.38 - case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
19.39 -}
19.40 -
19.41 -
19.42 -class HTML_Panel(
19.43 - sys: Isabelle_System,
19.44 - initial_font_size: Int,
19.45 - handler: PartialFunction[HTML_Panel.Event, Unit]) extends HtmlPanel
19.46 -{
19.47 - // global logging
19.48 - Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
19.49 -
19.50 -
19.51 - /* document template */
19.52 -
19.53 - private def try_file(name: String): String =
19.54 - {
19.55 - val file = sys.platform_file(name)
19.56 - if (file.isFile) Source.fromFile(file).mkString else ""
19.57 - }
19.58 -
19.59 - private def template(font_size: Int): String =
19.60 - """<?xml version="1.0" encoding="utf-8"?>
19.61 -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
19.62 - "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
19.63 -<html xmlns="http://www.w3.org/1999/xhtml">
19.64 -<head>
19.65 -<style media="all" type="text/css">
19.66 -""" +
19.67 - try_file("$ISABELLE_HOME/lib/html/isabelle.css") + "\n" +
19.68 - try_file("$ISABELLE_HOME_USER/etc/isabelle.css") + "\n" +
19.69 - "body { font-family: " + sys.font_family + "; font-size: " + font_size + "px }" +
19.70 -"""
19.71 -</style>
19.72 -</head>
19.73 -<body/>
19.74 -</html>
19.75 -"""
19.76 -
19.77 -
19.78 - /* actor with local state */
19.79 -
19.80 - private val ucontext = new SimpleUserAgentContext
19.81 -
19.82 - private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
19.83 - {
19.84 - private def handle(event: HTML_Panel.Event): Boolean =
19.85 - if (handler != null && handler.isDefinedAt(event)) { handler(event); true }
19.86 - else false
19.87 -
19.88 - override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
19.89 - handle(HTML_Panel.Context_Menu(elem, event))
19.90 - override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
19.91 - handle(HTML_Panel.Mouse_Click(elem, event))
19.92 - override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
19.93 - handle(HTML_Panel.Double_Click(elem, event))
19.94 - override def onMouseOver(elem: HTMLElement, event: MouseEvent)
19.95 - { handle(HTML_Panel.Mouse_Over(elem, event)) }
19.96 - override def onMouseOut(elem: HTMLElement, event: MouseEvent)
19.97 - { handle(HTML_Panel.Mouse_Out(elem, event)) }
19.98 - }
19.99 -
19.100 - private val builder = new DocumentBuilderImpl(ucontext, rcontext)
19.101 -
19.102 - private case class Init(font_size: Int)
19.103 - private case class Render(body: List[XML.Tree])
19.104 -
19.105 - private val main_actor = actor {
19.106 - // crude double buffering
19.107 - var doc1: org.w3c.dom.Document = null
19.108 - var doc2: org.w3c.dom.Document = null
19.109 -
19.110 - loop {
19.111 - react {
19.112 - case Init(font_size) =>
19.113 - val src = template(font_size)
19.114 - def parse() =
19.115 - builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
19.116 - doc1 = parse()
19.117 - doc2 = parse()
19.118 - Swing_Thread.now { setDocument(doc1, rcontext) }
19.119 -
19.120 - case Render(body) =>
19.121 - val doc = doc2
19.122 - val node =
19.123 - XML.document_node(doc,
19.124 - XML.elem(HTML.BODY, body.map((t: XML.Tree) => XML.elem(HTML.PRE, HTML.spans(t)))))
19.125 - doc.removeChild(doc.getLastChild())
19.126 - doc.appendChild(node)
19.127 - doc2 = doc1
19.128 - doc1 = doc
19.129 - Swing_Thread.now { setDocument(doc1, rcontext) }
19.130 -
19.131 - case bad => System.err.println("main_actor: ignoring bad message " + bad)
19.132 - }
19.133 - }
19.134 - }
19.135 -
19.136 - main_actor ! Init(initial_font_size)
19.137 -
19.138 -
19.139 - /* main method wrappers */
19.140 -
19.141 - def init(font_size: Int) { main_actor ! Init(font_size) }
19.142 - def render(body: List[XML.Tree]) { main_actor ! Render(body) }
19.143 -}
20.1 --- a/src/Tools/jEdit/src/proofdocument/markup_node.scala Mon Jan 11 22:44:21 2010 +0100
20.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
20.3 @@ -1,111 +0,0 @@
20.4 -/*
20.5 - * Document markup nodes, with connection to Swing tree model
20.6 - *
20.7 - * @author Fabian Immler, TU Munich
20.8 - * @author Makarius
20.9 - */
20.10 -
20.11 -package isabelle.proofdocument
20.12 -
20.13 -
20.14 -import javax.swing.tree.DefaultMutableTreeNode
20.15 -
20.16 -
20.17 -
20.18 -class Markup_Node(val start: Int, val stop: Int, val info: Any)
20.19 -{
20.20 - def fits_into(that: Markup_Node): Boolean =
20.21 - that.start <= this.start && this.stop <= that.stop
20.22 -}
20.23 -
20.24 -
20.25 -class Markup_Tree(val node: Markup_Node, val branches: List[Markup_Tree])
20.26 -{
20.27 - def set_branches(bs: List[Markup_Tree]): Markup_Tree = new Markup_Tree(node, bs)
20.28 -
20.29 - private def add(branch: Markup_Tree) = // FIXME avoid sort
20.30 - set_branches((branch :: branches) sort ((a, b) => a.node.start < b.node.start))
20.31 -
20.32 - private def remove(bs: List[Markup_Tree]) = set_branches(branches -- bs)
20.33 -
20.34 - def + (new_tree: Markup_Tree): Markup_Tree =
20.35 - {
20.36 - val new_node = new_tree.node
20.37 - if (new_node fits_into node) {
20.38 - var inserted = false
20.39 - val new_branches =
20.40 - branches.map(branch =>
20.41 - if ((new_node fits_into branch.node) && !inserted) {
20.42 - inserted = true
20.43 - branch + new_tree
20.44 - }
20.45 - else branch)
20.46 - if (!inserted) {
20.47 - // new_tree did not fit into children of this
20.48 - // -> insert between this and its branches
20.49 - val fitting = branches filter(_.node fits_into new_node)
20.50 - (this remove fitting) add ((new_tree /: fitting)(_ + _))
20.51 - }
20.52 - else set_branches(new_branches)
20.53 - }
20.54 - else {
20.55 - System.err.println("ignored nonfitting markup: " + new_node)
20.56 - this
20.57 - }
20.58 - }
20.59 -
20.60 - def flatten: List[Markup_Node] =
20.61 - {
20.62 - var next_x = node.start
20.63 - if (branches.isEmpty) List(this.node)
20.64 - else {
20.65 - val filled_gaps =
20.66 - for {
20.67 - child <- branches
20.68 - markups =
20.69 - if (next_x < child.node.start)
20.70 - new Markup_Node(next_x, child.node.start, node.info) :: child.flatten
20.71 - else child.flatten
20.72 - update = (next_x = child.node.stop)
20.73 - markup <- markups
20.74 - } yield markup
20.75 - if (next_x < node.stop)
20.76 - filled_gaps + new Markup_Node(next_x, node.stop, node.info)
20.77 - else filled_gaps
20.78 - }
20.79 - }
20.80 -}
20.81 -
20.82 -
20.83 -class Markup_Text(val markup: List[Markup_Tree], val content: String)
20.84 -{
20.85 - private lazy val root =
20.86 - new Markup_Tree(new Markup_Node(0, content.length, None), markup)
20.87 -
20.88 - def + (new_tree: Markup_Tree): Markup_Text =
20.89 - new Markup_Text((root + new_tree).branches, content)
20.90 -
20.91 - def filter(pred: Markup_Node => Boolean): Markup_Text =
20.92 - {
20.93 - def filt(tree: Markup_Tree): List[Markup_Tree] =
20.94 - {
20.95 - val branches = tree.branches.flatMap(filt(_))
20.96 - if (pred(tree.node)) List(tree.set_branches(branches))
20.97 - else branches
20.98 - }
20.99 - new Markup_Text(markup.flatMap(filt(_)), content)
20.100 - }
20.101 -
20.102 - def flatten: List[Markup_Node] = markup.flatten(_.flatten)
20.103 -
20.104 - def swing_tree(swing_node: Markup_Node => DefaultMutableTreeNode): DefaultMutableTreeNode =
20.105 - {
20.106 - def swing(tree: Markup_Tree): DefaultMutableTreeNode =
20.107 - {
20.108 - val node = swing_node(tree.node)
20.109 - tree.branches foreach ((branch: Markup_Tree) => node.add(swing(branch)))
20.110 - node
20.111 - }
20.112 - swing(root)
20.113 - }
20.114 -}
21.1 --- a/src/Tools/jEdit/src/proofdocument/session.scala Mon Jan 11 22:44:21 2010 +0100
21.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
21.3 @@ -1,250 +0,0 @@
21.4 -/*
21.5 - * Isabelle session, potentially with running prover
21.6 - *
21.7 - * @author Makarius
21.8 - */
21.9 -
21.10 -package isabelle.proofdocument
21.11 -
21.12 -
21.13 -import scala.actors.TIMEOUT
21.14 -import scala.actors.Actor._
21.15 -
21.16 -
21.17 -object Session
21.18 -{
21.19 - /* events */
21.20 -
21.21 - case object Global_Settings
21.22 -
21.23 -
21.24 - /* managed entities */
21.25 -
21.26 - type Entity_ID = String
21.27 -
21.28 - trait Entity
21.29 - {
21.30 - val id: Entity_ID
21.31 - def consume(session: Session, message: XML.Tree): Unit
21.32 - }
21.33 -}
21.34 -
21.35 -
21.36 -class Session(system: Isabelle_System)
21.37 -{
21.38 - /* pervasive event buses */
21.39 -
21.40 - val global_settings = new Event_Bus[Session.Global_Settings.type]
21.41 - val raw_results = new Event_Bus[Isabelle_Process.Result]
21.42 - val results = new Event_Bus[Command]
21.43 -
21.44 - val command_change = new Event_Bus[Command]
21.45 -
21.46 -
21.47 - /* unique ids */
21.48 -
21.49 - private var id_count: BigInt = 0
21.50 - def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
21.51 -
21.52 -
21.53 -
21.54 - /** main actor **/
21.55 -
21.56 - @volatile private var syntax = new Outer_Syntax(system.symbols)
21.57 - def current_syntax: Outer_Syntax = syntax
21.58 -
21.59 - @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
21.60 - def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
21.61 - def lookup_command(id: Session.Entity_ID): Option[Command] =
21.62 - lookup_entity(id) match {
21.63 - case Some(cmd: Command) => Some(cmd)
21.64 - case _ => None
21.65 - }
21.66 -
21.67 - private case class Start(timeout: Int, args: List[String])
21.68 - private case object Stop
21.69 - private case class Begin_Document(path: String)
21.70 -
21.71 - private val session_actor = actor {
21.72 -
21.73 - var prover: Isabelle_Process with Isar_Document = null
21.74 -
21.75 - def register(entity: Session.Entity) { entities += (entity.id -> entity) }
21.76 -
21.77 - var documents = Map[Isar_Document.Document_ID, Document]()
21.78 - def register_document(doc: Document) { documents += (doc.id -> doc) }
21.79 -
21.80 -
21.81 - /* document changes */
21.82 -
21.83 - def handle_change(change: Change)
21.84 - {
21.85 - require(change.parent.isDefined)
21.86 -
21.87 - val (changes, doc) = change.result.join
21.88 - val id_changes = changes map {
21.89 - case (c1, c2) =>
21.90 - (c1.map(_.id).getOrElse(""),
21.91 - c2 match {
21.92 - case None => None
21.93 - case Some(command) =>
21.94 - if (!lookup_command(command.id).isDefined) {
21.95 - register(command)
21.96 - prover.define_command(command.id, system.symbols.encode(command.source))
21.97 - }
21.98 - Some(command.id)
21.99 - })
21.100 - }
21.101 - register_document(doc)
21.102 - prover.edit_document(change.parent.get.id, doc.id, id_changes)
21.103 - }
21.104 -
21.105 -
21.106 - /* prover results */
21.107 -
21.108 - def bad_result(result: Isabelle_Process.Result)
21.109 - {
21.110 - System.err.println("Ignoring prover result: " + result)
21.111 - }
21.112 -
21.113 - def handle_result(result: Isabelle_Process.Result)
21.114 - {
21.115 - raw_results.event(result)
21.116 -
21.117 - val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
21.118 - val target: Option[Session.Entity] =
21.119 - target_id match {
21.120 - case None => None
21.121 - case Some(id) => lookup_entity(id)
21.122 - }
21.123 - if (target.isDefined) target.get.consume(this, result.message)
21.124 - else if (result.kind == Isabelle_Process.Kind.STATUS) {
21.125 - // global status message
21.126 - result.body match {
21.127 -
21.128 - // document state assigment
21.129 - case List(XML.Elem(Markup.ASSIGN, _, edits)) if target_id.isDefined =>
21.130 - documents.get(target_id.get) match {
21.131 - case Some(doc) =>
21.132 - val states =
21.133 - for {
21.134 - XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
21.135 - <- edits
21.136 - cmd <- lookup_command(cmd_id)
21.137 - } yield {
21.138 - val st = cmd.assign_state(state_id)
21.139 - register(st)
21.140 - (cmd, st)
21.141 - }
21.142 - doc.assign_states(states)
21.143 - case None => bad_result(result)
21.144 - }
21.145 -
21.146 - // command and keyword declarations
21.147 - case List(XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _)) =>
21.148 - syntax += (name, kind)
21.149 - case List(XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _)) =>
21.150 - syntax += name
21.151 -
21.152 - case _ => if (!result.is_ready) bad_result(result)
21.153 - }
21.154 - }
21.155 - else if (result.kind == Isabelle_Process.Kind.EXIT)
21.156 - prover = null
21.157 - else if (result.kind != Isabelle_Process.Kind.STDIN && !result.is_raw)
21.158 - bad_result(result)
21.159 - }
21.160 -
21.161 -
21.162 - /* prover startup */
21.163 -
21.164 - def startup_error(): String =
21.165 - {
21.166 - val buf = new StringBuilder
21.167 - while (
21.168 - receiveWithin(0) {
21.169 - case result: Isabelle_Process.Result =>
21.170 - if (result.is_raw) {
21.171 - for (text <- XML.content(result.message))
21.172 - buf.append(text)
21.173 - }
21.174 - true
21.175 - case TIMEOUT => false
21.176 - }) {}
21.177 - buf.toString
21.178 - }
21.179 -
21.180 - def prover_startup(timeout: Int): Option[String] =
21.181 - {
21.182 - receiveWithin(timeout) {
21.183 - case result: Isabelle_Process.Result
21.184 - if result.kind == Isabelle_Process.Kind.INIT =>
21.185 - while (receive {
21.186 - case result: Isabelle_Process.Result =>
21.187 - handle_result(result); !result.is_ready
21.188 - }) {}
21.189 - None
21.190 -
21.191 - case result: Isabelle_Process.Result
21.192 - if result.kind == Isabelle_Process.Kind.EXIT =>
21.193 - Some(startup_error())
21.194 -
21.195 - case TIMEOUT => // FIXME clarify
21.196 - prover.kill; Some(startup_error())
21.197 - }
21.198 - }
21.199 -
21.200 -
21.201 - /* main loop */
21.202 -
21.203 - val xml_cache = new XML.Cache(131071)
21.204 -
21.205 - loop {
21.206 - react {
21.207 - case Start(timeout, args) =>
21.208 - if (prover == null) {
21.209 - prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
21.210 - val origin = sender
21.211 - val opt_err = prover_startup(timeout)
21.212 - if (opt_err.isDefined) prover = null
21.213 - origin ! opt_err
21.214 - }
21.215 - else reply(None)
21.216 -
21.217 - case Stop => // FIXME clarify; synchronous
21.218 - if (prover != null) {
21.219 - prover.kill
21.220 - prover = null
21.221 - }
21.222 -
21.223 - case Begin_Document(path: String) if prover != null =>
21.224 - val id = create_id()
21.225 - val doc = Document.empty(id)
21.226 - register_document(doc)
21.227 - prover.begin_document(id, path)
21.228 - reply(doc)
21.229 -
21.230 - case change: Change if prover != null =>
21.231 - handle_change(change)
21.232 -
21.233 - case result: Isabelle_Process.Result =>
21.234 - handle_result(result.cache(xml_cache))
21.235 -
21.236 - case bad if prover != null =>
21.237 - System.err.println("session_actor: ignoring bad message " + bad)
21.238 - }
21.239 - }
21.240 - }
21.241 -
21.242 -
21.243 - /* main methods */
21.244 -
21.245 - def start(timeout: Int, args: List[String]): Option[String] =
21.246 - (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]
21.247 -
21.248 - def stop() { session_actor ! Stop }
21.249 - def input(change: Change) { session_actor ! change }
21.250 -
21.251 - def begin_document(path: String): Document =
21.252 - (session_actor !? Begin_Document(path)).asInstanceOf[Document]
21.253 -}
22.1 --- a/src/Tools/jEdit/src/proofdocument/state.scala Mon Jan 11 22:44:21 2010 +0100
22.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
22.3 @@ -1,117 +0,0 @@
22.4 -/*
22.5 - * Accumulating results from prover
22.6 - *
22.7 - * @author Fabian Immler, TU Munich
22.8 - * @author Makarius
22.9 - */
22.10 -
22.11 -package isabelle.proofdocument
22.12 -
22.13 -
22.14 -class State(
22.15 - val command: Command,
22.16 - val status: Command.Status.Value,
22.17 - val rev_results: List[XML.Tree],
22.18 - val markup_root: Markup_Text)
22.19 -{
22.20 - def this(command: Command) =
22.21 - this(command, Command.Status.UNPROCESSED, Nil, command.empty_markup)
22.22 -
22.23 -
22.24 - /* content */
22.25 -
22.26 - private def set_status(st: Command.Status.Value): State =
22.27 - new State(command, st, rev_results, markup_root)
22.28 -
22.29 - private def add_result(res: XML.Tree): State =
22.30 - new State(command, status, res :: rev_results, markup_root)
22.31 -
22.32 - private def add_markup(node: Markup_Tree): State =
22.33 - new State(command, status, rev_results, markup_root + node)
22.34 -
22.35 - lazy val results = rev_results.reverse
22.36 -
22.37 -
22.38 - /* markup */
22.39 -
22.40 - lazy val highlight: Markup_Text =
22.41 - {
22.42 - markup_root.filter(_.info match {
22.43 - case Command.HighlightInfo(_) => true
22.44 - case _ => false
22.45 - })
22.46 - }
22.47 -
22.48 - private lazy val types: List[Markup_Node] =
22.49 - markup_root.filter(_.info match {
22.50 - case Command.TypeInfo(_) => true
22.51 - case _ => false }).flatten
22.52 -
22.53 - def type_at(pos: Int): Option[String] =
22.54 - {
22.55 - types.find(t => t.start <= pos && pos < t.stop) match {
22.56 - case Some(t) =>
22.57 - t.info match {
22.58 - case Command.TypeInfo(ty) => Some(command.source(t.start, t.stop) + ": " + ty)
22.59 - case _ => None
22.60 - }
22.61 - case None => None
22.62 - }
22.63 - }
22.64 -
22.65 - private lazy val refs: List[Markup_Node] =
22.66 - markup_root.filter(_.info match {
22.67 - case Command.RefInfo(_, _, _, _) => true
22.68 - case _ => false }).flatten
22.69 -
22.70 - def ref_at(pos: Int): Option[Markup_Node] =
22.71 - refs.find(t => t.start <= pos && pos < t.stop)
22.72 -
22.73 -
22.74 - /* message dispatch */
22.75 -
22.76 - def + (session: Session, message: XML.Tree): State =
22.77 - {
22.78 - val changed: State =
22.79 - message match {
22.80 - case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
22.81 - (this /: elems)((state, elem) =>
22.82 - elem match {
22.83 - case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
22.84 - case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
22.85 - case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
22.86 - case XML.Elem(kind, atts, body) =>
22.87 - val (begin, end) = Position.get_offsets(atts)
22.88 - if (begin.isEmpty || end.isEmpty) state
22.89 - else if (kind == Markup.ML_TYPING) {
22.90 - val info = body.first.asInstanceOf[XML.Text].content // FIXME proper match!?
22.91 - state.add_markup(
22.92 - command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
22.93 - }
22.94 - else if (kind == Markup.ML_REF) {
22.95 - body match {
22.96 - case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
22.97 - state.add_markup(command.markup_node(
22.98 - begin.get - 1, end.get - 1,
22.99 - Command.RefInfo(
22.100 - Position.get_file(atts),
22.101 - Position.get_line(atts),
22.102 - Position.get_id(atts),
22.103 - Position.get_offset(atts))))
22.104 - case _ => state
22.105 - }
22.106 - }
22.107 - else {
22.108 - state.add_markup(
22.109 - command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
22.110 - }
22.111 - case _ =>
22.112 - System.err.println("ignored status report: " + elem)
22.113 - state
22.114 - })
22.115 - case _ => add_result(message)
22.116 - }
22.117 - if (!(this eq changed)) session.command_change.event(command)
22.118 - changed
22.119 - }
22.120 -}