incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
authorwenzelm
Mon Jan 11 23:00:05 2010 +0100 (2010-01-11 ago)
changeset 34871e596a0b71f3c
parent 34870 e10547372c41
child 34875 45aa70e7e7b6
incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
src/Pure/General/xml.scala
src/Pure/System/session.scala
src/Pure/Thy/change.scala
src/Pure/Thy/command.scala
src/Pure/Thy/document.scala
src/Pure/Thy/markup_node.scala
src/Pure/Thy/state.scala
src/Pure/build-jars
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/html_panel.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/output_dockable.scala
src/Tools/jEdit/src/jedit/plugin.scala
src/Tools/jEdit/src/proofdocument/change.scala
src/Tools/jEdit/src/proofdocument/command.scala
src/Tools/jEdit/src/proofdocument/document.scala
src/Tools/jEdit/src/proofdocument/html_panel.scala
src/Tools/jEdit/src/proofdocument/markup_node.scala
src/Tools/jEdit/src/proofdocument/session.scala
src/Tools/jEdit/src/proofdocument/state.scala
     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 -}