class Session models full session, with or without prover process (cf. heaps, browser_info);
authorwenzelm
Thu Dec 10 22:15:19 2009 +0100 (2009-12-10 ago)
changeset 3477791d6089cef88
parent 34776 01a9bfd64b87
child 34778 8eccd35e975e
class Session models full session, with or without prover process (cf. heaps, browser_info);
replaced Prover by Session, with a singleton instance in Isabelle plugin (shared by all active buffers);
misc cleanup of Session vs. Plugin instance;
eliminated Prover_Setup -- maintain mapping of JEditBuffer <-> Theory_View directly;
misc tuning and simplification;
src/Tools/jEdit/src/jedit/document_overview.scala
src/Tools/jEdit/src/jedit/history_dockable.scala
src/Tools/jEdit/src/jedit/isabelle_encoding.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
src/Tools/jEdit/src/jedit/output_dockable.scala
src/Tools/jEdit/src/jedit/plugin.scala
src/Tools/jEdit/src/jedit/protocol_dockable.scala
src/Tools/jEdit/src/jedit/prover_setup.scala
src/Tools/jEdit/src/proofdocument/command.scala
src/Tools/jEdit/src/proofdocument/prover.scala
src/Tools/jEdit/src/proofdocument/session.scala
src/Tools/jEdit/src/proofdocument/state.scala
src/Tools/jEdit/src/proofdocument/theory_view.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/document_overview.scala	Thu Dec 10 14:23:28 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_overview.scala	Thu Dec 10 22:15:19 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  package isabelle.jedit
     1.5  
     1.6  
     1.7 -import isabelle.proofdocument.{Command, Proof_Document, Prover, Theory_View}
     1.8 +import isabelle.proofdocument.{Command, Proof_Document, Theory_View}
     1.9  
    1.10  import javax.swing.{JPanel, ToolTipManager}
    1.11  import java.awt.event.{MouseAdapter, MouseEvent}
    1.12 @@ -15,11 +15,9 @@
    1.13  
    1.14  import org.gjt.sp.jedit.gui.RolloverButton
    1.15  import org.gjt.sp.jedit.textarea.JEditTextArea
    1.16 -import org.gjt.sp.jedit.buffer.JEditBuffer
    1.17  
    1.18  
    1.19  class Document_Overview(
    1.20 -    prover: Prover,
    1.21      text_area: JEditTextArea,
    1.22      to_current: (Proof_Document, Int) => Int)
    1.23    extends JPanel(new BorderLayout)
    1.24 @@ -56,10 +54,11 @@
    1.25      else ""
    1.26    }
    1.27  
    1.28 -  override def paintComponent(gfx: Graphics) {
    1.29 +  override def paintComponent(gfx: Graphics)
    1.30 +  {
    1.31      super.paintComponent(gfx)
    1.32      val buffer = text_area.getBuffer
    1.33 -    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
    1.34 +    val theory_view = Isabelle.plugin.theory_view(buffer).get
    1.35      val doc = theory_view.current_document()
    1.36  
    1.37      for (command <- doc.commands) {
     2.1 --- a/src/Tools/jEdit/src/jedit/history_dockable.scala	Thu Dec 10 14:23:28 2009 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/history_dockable.scala	Thu Dec 10 22:15:19 2009 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  package isabelle.jedit
     2.5  
     2.6  
     2.7 -import isabelle.proofdocument.Change
     2.8 +import isabelle.proofdocument.{Change, Theory_View}
     2.9  
    2.10  import java.awt.Dimension
    2.11  import scala.swing.{ListView, FlowPanel}
    2.12 @@ -22,11 +22,12 @@
    2.13    if (position == DockableWindowManager.FLOATING)
    2.14      preferredSize = new Dimension(500, 250)
    2.15  
    2.16 -  def prover_setup(): Option[Prover_Setup] = Isabelle.prover_setup(view.getBuffer)
    2.17 +  def dynamic_theory_view(): Option[Theory_View] =
    2.18 +    Isabelle.plugin.theory_view(view.getBuffer)
    2.19    def get_versions() =
    2.20 -    prover_setup() match {
    2.21 +    dynamic_theory_view() match {
    2.22        case None => Nil
    2.23 -      case Some(setup) => setup.theory_view.changes
    2.24 +      case Some(theory_view) => theory_view.changes
    2.25      }
    2.26  
    2.27    val list = new ListView[Change]
    2.28 @@ -37,8 +38,9 @@
    2.29    listenTo(list.selection)
    2.30    reactions += {
    2.31      case ListSelectionChanged(source, range, false) =>
    2.32 -      prover_setup().map(_.theory_view.set_version(list.listData(range.start)))
    2.33 +      dynamic_theory_view().map(_.set_version(list.listData(range.start)))
    2.34    }
    2.35  
    2.36 -  prover_setup.foreach(_.prover.document_change += (_ => list.listData = get_versions()))
    2.37 +  if (dynamic_theory_view().isDefined)
    2.38 +    Isabelle.session.document_change += (_ => list.listData = get_versions())
    2.39  }
     3.1 --- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Thu Dec 10 14:23:28 2009 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Thu Dec 10 22:15:19 2009 +0100
     3.3 @@ -34,7 +34,7 @@
     3.4    {
     3.5      def source(): Source =
     3.6        BufferedSource.fromInputStream(in, decoder, BUFSIZE, { () => source() })
     3.7 -    new CharArrayReader(Isabelle.symbols.decode(source.mkString).toArray)
     3.8 +    new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
     3.9    }
    3.10  
    3.11  	override def getTextReader(in: InputStream): Reader =
    3.12 @@ -53,7 +53,7 @@
    3.13      val buffer = new ByteArrayOutputStream(BUFSIZE) {
    3.14        override def flush()
    3.15        {
    3.16 -        val text = Isabelle.symbols.encode(toString(Isabelle_System.charset))
    3.17 +        val text = Isabelle.system.symbols.encode(toString(Isabelle_System.charset))
    3.18          out.write(text.getBytes(Isabelle_System.charset))
    3.19          out.flush()
    3.20        }
     4.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Dec 10 14:23:28 2009 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Dec 10 22:15:19 2009 +0100
     4.3 @@ -45,38 +45,35 @@
     4.4  {
     4.5  	def getHyperlink(buffer: Buffer, original_offset: Int): Hyperlink =
     4.6  	{
     4.7 -    val prover = Isabelle.prover_setup(buffer).map(_.prover)
     4.8 -    val theory_view_opt = Isabelle.prover_setup(buffer).map(_.theory_view)
     4.9 -    if (prover.isEmpty || theory_view_opt.isEmpty) null
    4.10 -    else if (prover.get == null || theory_view_opt.get == null) null
    4.11 -    else {
    4.12 -      val theory_view = theory_view_opt.get
    4.13 -      val document = theory_view.current_document()
    4.14 -      val offset = theory_view.from_current(document, original_offset)
    4.15 -      document.command_at(offset) match {
    4.16 -        case Some(command) =>
    4.17 -          command.ref_at(document, offset - command.start(document)) match {
    4.18 -            case Some(ref) =>
    4.19 -              val command_start = command.start(document)
    4.20 -              val begin = theory_view.to_current(document, command_start + ref.start)
    4.21 -              val line = buffer.getLineOfOffset(begin)
    4.22 -              val end = theory_view.to_current(document, command_start + ref.stop)
    4.23 -              ref.info match {
    4.24 -                case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    4.25 -                  new External_Hyperlink(begin, end, line, ref_file, ref_line)
    4.26 -                case Command.RefInfo(_, _, Some(id), Some(offset)) =>
    4.27 -                  prover.get.command(id) match {
    4.28 -                    case Some(ref_cmd) =>
    4.29 -                      new Internal_Hyperlink(begin, end, line,
    4.30 -                        theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
    4.31 -                    case None => null
    4.32 -                  }
    4.33 -                case _ => null
    4.34 -              }
    4.35 -            case None => null
    4.36 -          }
    4.37 -        case None => null
    4.38 -      }
    4.39 +    Isabelle.plugin.theory_view(buffer) match {
    4.40 +      case Some(theory_view) =>
    4.41 +        val document = theory_view.current_document()
    4.42 +        val offset = theory_view.from_current(document, original_offset)
    4.43 +        document.command_at(offset) match {
    4.44 +          case Some(command) =>
    4.45 +            command.ref_at(document, offset - command.start(document)) match {
    4.46 +              case Some(ref) =>
    4.47 +                val command_start = command.start(document)
    4.48 +                val begin = theory_view.to_current(document, command_start + ref.start)
    4.49 +                val line = buffer.getLineOfOffset(begin)
    4.50 +                val end = theory_view.to_current(document, command_start + ref.stop)
    4.51 +                ref.info match {
    4.52 +                  case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
    4.53 +                    new External_Hyperlink(begin, end, line, ref_file, ref_line)
    4.54 +                  case Command.RefInfo(_, _, Some(id), Some(offset)) =>
    4.55 +                    Isabelle.session.command(id) match {
    4.56 +                      case Some(ref_cmd) =>
    4.57 +                        new Internal_Hyperlink(begin, end, line,
    4.58 +                          theory_view.to_current(document, ref_cmd.start(document) + offset - 1))
    4.59 +                      case None => null
    4.60 +                    }
    4.61 +                  case _ => null
    4.62 +                }
    4.63 +              case None => null
    4.64 +            }
    4.65 +          case None => null
    4.66 +        }
    4.67 +      case None => null
    4.68      }
    4.69    }
    4.70  }
     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Dec 10 14:23:28 2009 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Dec 10 22:15:19 2009 +0100
     5.3 @@ -40,38 +40,37 @@
     5.4      val root = data.root
     5.5      data.getAsset(root).setEnd(buffer.getLength)
     5.6  
     5.7 -    val prover_setup = Isabelle.prover_setup(buffer)
     5.8 -    if (prover_setup.isDefined) {
     5.9 -      val document = prover_setup.get.theory_view.current_document()
    5.10 -      for (command <- document.commands if !stopped) {
    5.11 -        root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
    5.12 -            {
    5.13 -              val content = command.content(node.start, node.stop)
    5.14 -              val command_start = command.start(document)
    5.15 -              val id = command.id
    5.16 +    Isabelle.plugin.theory_view(buffer) match {
    5.17 +      case Some(theory_view) =>
    5.18 +        val document = theory_view.current_document()
    5.19 +        for (command <- document.commands if !stopped) {
    5.20 +          root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
    5.21 +              {
    5.22 +                val content = command.content(node.start, node.stop)
    5.23 +                val command_start = command.start(document)
    5.24 +                val id = command.id
    5.25  
    5.26 -              new DefaultMutableTreeNode(new IAsset {
    5.27 -                override def getIcon: Icon = null
    5.28 -                override def getShortString: String = content
    5.29 -                override def getLongString: String = node.info.toString
    5.30 -                override def getName: String = id
    5.31 -                override def setName(name: String) = ()
    5.32 -                override def setStart(start: Position) = ()
    5.33 -                override def getStart: Position = command_start + node.start
    5.34 -                override def setEnd(end: Position) = ()
    5.35 -                override def getEnd: Position = command_start + node.stop
    5.36 -                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    5.37 -              })
    5.38 -            }))
    5.39 -      }
    5.40 -      if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    5.41 +                new DefaultMutableTreeNode(new IAsset {
    5.42 +                  override def getIcon: Icon = null
    5.43 +                  override def getShortString: String = content
    5.44 +                  override def getLongString: String = node.info.toString
    5.45 +                  override def getName: String = id
    5.46 +                  override def setName(name: String) = ()
    5.47 +                  override def setStart(start: Position) = ()
    5.48 +                  override def getStart: Position = command_start + node.start
    5.49 +                  override def setEnd(end: Position) = ()
    5.50 +                  override def getEnd: Position = command_start + node.stop
    5.51 +                  override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    5.52 +                })
    5.53 +              }))
    5.54 +        }
    5.55 +        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    5.56 +      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    5.57      }
    5.58 -    else root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    5.59 -
    5.60      data
    5.61    }
    5.62  
    5.63 -
    5.64 +  
    5.65    /* completion */
    5.66  
    5.67    override def supportsCompletion = true
    5.68 @@ -85,8 +84,7 @@
    5.69      val start = buffer.getLineStartOffset(line)
    5.70      val text = buffer.getSegment(start, caret - start)
    5.71  
    5.72 -    val completion =
    5.73 -      Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion)
    5.74 +    val completion = Isabelle.session.completion()
    5.75  
    5.76      completion.complete(text) match {
    5.77        case None => null
     6.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Dec 10 14:23:28 2009 +0100
     6.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Dec 10 22:15:19 2009 +0100
     6.3 @@ -8,7 +8,6 @@
     6.4  package isabelle.jedit
     6.5  
     6.6  
     6.7 -import isabelle.proofdocument.Prover
     6.8  import isabelle.Markup
     6.9  
    6.10  import org.gjt.sp.jedit.buffer.JEditBuffer
    6.11 @@ -100,7 +99,7 @@
    6.12  }
    6.13  
    6.14  
    6.15 -class Isabelle_Token_Marker(buffer: JEditBuffer, prover: Prover) extends TokenMarker
    6.16 +class Isabelle_Token_Marker(buffer: JEditBuffer) extends TokenMarker
    6.17  {
    6.18    override def markTokens(prev: TokenMarker.LineContext,
    6.19        handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
    6.20 @@ -111,7 +110,7 @@
    6.21      val start = buffer.getLineStartOffset(line)
    6.22      val stop = start + line_segment.count
    6.23  
    6.24 -    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
    6.25 +    val theory_view = Isabelle.plugin.theory_view(buffer).get  // FIXME total?
    6.26      val document = theory_view.current_document()
    6.27      def to: Int => Int = theory_view.to_current(document, _)
    6.28      def from: Int => Int = theory_view.from_current(document, _)
     7.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Dec 10 14:23:28 2009 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Dec 10 22:15:19 2009 +0100
     7.3 @@ -42,11 +42,15 @@
     7.4      loop {
     7.5        react {
     7.6          case cmd: Command =>
     7.7 -          val theory_view = Isabelle.prover_setup(view.getBuffer).get.theory_view
     7.8 -          val body =
     7.9 -            if (cmd == null) Nil  // FIXME ??
    7.10 -            else cmd.results(theory_view.current_document)
    7.11 -          html_panel.render(body)
    7.12 +          Isabelle.plugin.theory_view(view.getBuffer)  // FIXME total!?!
    7.13 +          match {
    7.14 +            case None =>
    7.15 +            case Some(theory_view) =>
    7.16 +              val body =
    7.17 +                if (cmd == null) Nil  // FIXME ??
    7.18 +                else cmd.results(theory_view.current_document)
    7.19 +              html_panel.render(body)
    7.20 +          }
    7.21            
    7.22          case bad => System.err.println("output_actor: ignoring bad message " + bad)
    7.23        }
    7.24 @@ -62,15 +66,17 @@
    7.25      }
    7.26    }
    7.27  
    7.28 -  override def addNotify() {
    7.29 +  override def addNotify()
    7.30 +  {
    7.31      super.addNotify()
    7.32 -    Isabelle.plugin.state_update += output_actor
    7.33 -    Isabelle.plugin.properties_changed += properties_actor
    7.34 +    Isabelle.session.results += output_actor
    7.35 +    Isabelle.session.global_settings += properties_actor
    7.36    }
    7.37  
    7.38 -  override def removeNotify() {
    7.39 -    Isabelle.plugin.state_update -= output_actor
    7.40 -    Isabelle.plugin.properties_changed -= properties_actor
    7.41 +  override def removeNotify()
    7.42 +  {
    7.43 +    Isabelle.session.results -= output_actor
    7.44 +    Isabelle.session.global_settings -= properties_actor
    7.45      super.removeNotify()
    7.46    }
    7.47  }
     8.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Dec 10 14:23:28 2009 +0100
     8.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Dec 10 22:15:19 2009 +0100
     8.3 @@ -9,15 +9,14 @@
     8.4  package isabelle.jedit
     8.5  
     8.6  
     8.7 +import isabelle.proofdocument.{Session, Theory_View}
     8.8 +
     8.9  import java.io.{FileInputStream, IOException}
    8.10  import java.awt.Font
    8.11  import javax.swing.JScrollPane
    8.12  
    8.13  import scala.collection.mutable
    8.14  
    8.15 -import isabelle.proofdocument.{Command, Proof_Document, Prover}
    8.16 -import isabelle.Isabelle_System
    8.17 -
    8.18  import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
    8.19  import org.gjt.sp.jedit.buffer.JEditBuffer
    8.20  import org.gjt.sp.jedit.textarea.JEditTextArea
    8.21 @@ -54,16 +53,9 @@
    8.22    }
    8.23  
    8.24  
    8.25 -  /* Isabelle system instance */
    8.26 -
    8.27 -  var system: Isabelle_System = null
    8.28 -  def symbols = system.symbols
    8.29 -  lazy val completion = new Completion + symbols
    8.30 -
    8.31 -
    8.32    /* settings */
    8.33  
    8.34 -  def default_logic(): String =
    8.35 +  def get_logic(): String =
    8.36    {
    8.37      val logic = Isabelle.Property("logic")
    8.38      if (logic != null) logic
    8.39 @@ -74,51 +66,44 @@
    8.40    /* plugin instance */
    8.41  
    8.42    var plugin: Plugin = null
    8.43 -
    8.44 -
    8.45 -  /* running provers */
    8.46 -
    8.47 -  def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
    8.48 +  var system: Isabelle_System = null
    8.49 +  var session: Session = null
    8.50  }
    8.51  
    8.52  
    8.53  class Plugin extends EBPlugin
    8.54  {
    8.55 -  /* event buses */
    8.56 -
    8.57 -  val properties_changed = new Event_Bus[Unit]
    8.58 -  val raw_results = new Event_Bus[Isabelle_Process.Result]
    8.59 -  val state_update = new Event_Bus[Command]
    8.60 -
    8.61 -
    8.62 -  /* selected state */
    8.63 +  /* mapping buffer <-> theory view */
    8.64  
    8.65 -  private var _selected_state: Command = null
    8.66 -  def selected_state = _selected_state
    8.67 -  def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
    8.68 -
    8.69 -
    8.70 -  /* mapping buffer <-> prover */
    8.71 -
    8.72 -  private val mapping = new mutable.HashMap[JEditBuffer, Prover_Setup]
    8.73 +  private var mapping = Map[JEditBuffer, Theory_View]()
    8.74  
    8.75    private def install(view: View)
    8.76    {
    8.77 +    val text_area = view.getTextArea
    8.78      val buffer = view.getBuffer
    8.79 -    val prover_setup = new Prover_Setup(buffer)
    8.80 -    mapping.update(buffer, prover_setup)
    8.81 -    prover_setup.activate(view)
    8.82 +
    8.83 + 
    8.84 +    val theory_view = new Theory_View(Isabelle.session, text_area)   // FIXME multiple text areas!?
    8.85 +    mapping += (buffer -> theory_view)
    8.86 +
    8.87 +    Isabelle.session.start(Isabelle.get_logic())
    8.88 +    theory_view.activate()
    8.89 +    Isabelle.session.begin_document(buffer.getName)
    8.90    }
    8.91  
    8.92 -  private def uninstall(view: View) =
    8.93 -    mapping.removeKey(view.getBuffer).get.deactivate
    8.94 +  private def uninstall(view: View)
    8.95 +  {
    8.96 +    val buffer = view.getBuffer
    8.97 +    mapping(buffer).deactivate
    8.98 +    mapping -= buffer
    8.99 +  }
   8.100  
   8.101    def switch_active(view: View) =
   8.102      if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
   8.103      else install(view)
   8.104  
   8.105 -  def prover_setup(buffer: JEditBuffer): Option[Prover_Setup] = mapping.get(buffer)
   8.106 -  def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
   8.107 +  def theory_view(buffer: JEditBuffer): Option[Theory_View] = mapping.get(buffer)
   8.108 +  def is_active(buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
   8.109  
   8.110  
   8.111    /* main plugin plumbing */
   8.112 @@ -130,13 +115,14 @@
   8.113          val buffer = msg.getEditPane.getBuffer
   8.114          msg.getWhat match {
   8.115            case EditPaneUpdate.BUFFER_CHANGED =>
   8.116 -            (mapping get buffer) map (_.theory_view.activate)
   8.117 +            theory_view(buffer)map(_.activate)
   8.118            case EditPaneUpdate.BUFFER_CHANGING =>
   8.119              if (buffer != null)
   8.120 -              (mapping get buffer) map (_.theory_view.deactivate)
   8.121 +              theory_view(buffer).map(_.deactivate)
   8.122            case _ =>
   8.123          }
   8.124 -      case msg: PropertiesChanged => properties_changed.event(())
   8.125 +      case msg: PropertiesChanged =>
   8.126 +        Isabelle.session.global_settings.event(())
   8.127        case _ =>
   8.128      }
   8.129    }
   8.130 @@ -146,11 +132,13 @@
   8.131      Isabelle.plugin = this
   8.132      Isabelle.system = new Isabelle_System
   8.133      Isabelle.system.install_fonts()
   8.134 +    Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
   8.135    }
   8.136  
   8.137    override def stop()
   8.138    {
   8.139 -    // TODO: proper cleanup
   8.140 +    Isabelle.session.stop()  // FIXME dialog!?
   8.141 +    Isabelle.session = null
   8.142      Isabelle.system = null
   8.143      Isabelle.plugin = null
   8.144    }
     9.1 --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Thu Dec 10 14:23:28 2009 +0100
     9.2 +++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Thu Dec 10 22:15:19 2009 +0100
     9.3 @@ -48,12 +48,12 @@
     9.4    override def addNotify()
     9.5    {
     9.6      super.addNotify()
     9.7 -    Isabelle.plugin.raw_results += raw_actor
     9.8 +    Isabelle.session.raw_results += raw_actor
     9.9    }
    9.10  
    9.11    override def removeNotify()
    9.12    {
    9.13 -    Isabelle.plugin.raw_results -= raw_actor
    9.14 +    Isabelle.session.raw_results -= raw_actor
    9.15      super.removeNotify()
    9.16    }
    9.17  }
    10.1 --- a/src/Tools/jEdit/src/jedit/prover_setup.scala	Thu Dec 10 14:23:28 2009 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,35 +0,0 @@
    10.4 -/*
    10.5 - * Independent prover sessions for each buffer
    10.6 - *
    10.7 - * @author Fabian Immler, TU Munich
    10.8 - */
    10.9 -
   10.10 -package isabelle.jedit
   10.11 -
   10.12 -
   10.13 -import org.gjt.sp.jedit.{Buffer, View}
   10.14 -
   10.15 -import isabelle.proofdocument.{Prover, Theory_View}
   10.16 -
   10.17 -
   10.18 -class Prover_Setup(buffer: Buffer)
   10.19 -{
   10.20 -  var prover: Prover = null
   10.21 -  var theory_view: Theory_View = null
   10.22 -
   10.23 -  def activate(view: View)
   10.24 -  {
   10.25 -    // Theory_View starts prover
   10.26 -    theory_view = new Theory_View(view.getTextArea)
   10.27 -    prover = theory_view.prover
   10.28 -
   10.29 -    theory_view.activate()
   10.30 -    prover.begin_document(buffer.getName)
   10.31 -  }
   10.32 -
   10.33 -  def deactivate()
   10.34 -  {
   10.35 -    theory_view.deactivate
   10.36 -    prover.stop
   10.37 -  }
   10.38 -}
    11.1 --- a/src/Tools/jEdit/src/proofdocument/command.scala	Thu Dec 10 14:23:28 2009 +0100
    11.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala	Thu Dec 10 22:15:19 2009 +0100
    11.3 @@ -12,7 +12,7 @@
    11.4  
    11.5  import scala.collection.mutable
    11.6  
    11.7 -import isabelle.jedit.{Isabelle, Plugin}
    11.8 +import isabelle.jedit.Isabelle
    11.9  import isabelle.XML
   11.10  
   11.11  
   11.12 @@ -26,7 +26,7 @@
   11.13    override def act() {
   11.14      loop {
   11.15        react {
   11.16 -        case (prover: Prover, message: XML.Tree) => _state = _state.+(prover, message)
   11.17 +        case (session: Session, message: XML.Tree) => _state = _state.+(session, message)
   11.18          case bad => System.err.println("Accumulator: ignoring bad message " + bad)
   11.19        }
   11.20      }
    12.1 --- a/src/Tools/jEdit/src/proofdocument/prover.scala	Thu Dec 10 14:23:28 2009 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,170 +0,0 @@
    12.4 -/*
    12.5 - * Higher-level prover communication: interactive document model
    12.6 - *
    12.7 - * @author Johannes Hölzl, TU Munich
    12.8 - * @author Fabian Immler, TU Munich
    12.9 - * @author Makarius
   12.10 - */
   12.11 -
   12.12 -package isabelle.proofdocument
   12.13 -
   12.14 -
   12.15 -import scala.actors.Actor, Actor._
   12.16 -
   12.17 -import javax.swing.JTextArea
   12.18 -
   12.19 -import isabelle.jedit.Isabelle
   12.20 -
   12.21 -
   12.22 -class Prover(system: Isabelle_System, logic: String)
   12.23 -{
   12.24 -  /* incoming messages */
   12.25 -
   12.26 -  private var prover_ready = false
   12.27 -
   12.28 -  private val receiver = new Actor {
   12.29 -    def act() {
   12.30 -      loop {
   12.31 -        react {
   12.32 -          case result: Isabelle_Process.Result => handle_result(result)
   12.33 -          case change: Change if prover_ready => handle_change(change)
   12.34 -          case bad if prover_ready => System.err.println("receiver: ignoring bad message " + bad)
   12.35 -        }
   12.36 -      }
   12.37 -    }
   12.38 -  }
   12.39 -
   12.40 -  def input(change: Change) { receiver ! change }
   12.41 -
   12.42 -
   12.43 -  /* outgoing messages */
   12.44 -
   12.45 -  val command_change = new Event_Bus[Command]
   12.46 -  val document_change = new Event_Bus[Proof_Document]
   12.47 -
   12.48 -
   12.49 -  /* prover process */
   12.50 -
   12.51 -  private val process =
   12.52 -    new Isabelle_Process(system, receiver, "-m", "xsymbols", logic) with Isar_Document
   12.53 -
   12.54 -
   12.55 -  /* outer syntax keywords and completion */
   12.56 -
   12.57 -  @volatile private var _command_decls = Map[String, String]()
   12.58 -  def command_decls() = _command_decls
   12.59 -
   12.60 -  @volatile private var _keyword_decls = Set[String]()
   12.61 -  def keyword_decls() = _keyword_decls
   12.62 -
   12.63 -  @volatile private var _completion = Isabelle.completion
   12.64 -  def completion() = _completion
   12.65 -
   12.66 -
   12.67 -  /* document state information */
   12.68 -
   12.69 -  @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
   12.70 -  @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
   12.71 -  val document_0 =
   12.72 -    Proof_Document.empty.
   12.73 -    set_command_keyword((s: String) => command_decls().contains(s))
   12.74 -  @volatile private var document_versions = List(document_0)
   12.75 -
   12.76 -  def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
   12.77 -  def document(id: Isar_Document.Document_ID): Option[Proof_Document] =
   12.78 -    document_versions.find(_.id == id)
   12.79 -
   12.80 -
   12.81 -  /* prover results */
   12.82 -
   12.83 -  private def handle_result(result: Isabelle_Process.Result)
   12.84 -  {
   12.85 -    Isabelle.plugin.raw_results.event(result)
   12.86 -    val message = Isabelle_Process.parse_message(system, result)
   12.87 -
   12.88 -    val state =
   12.89 -      Position.id_of(result.props) match {
   12.90 -        case None => None
   12.91 -        case Some(id) => commands.get(id) orElse states.get(id) orElse None
   12.92 -      }
   12.93 -    if (state.isDefined) state.get ! (this, message)
   12.94 -    else if (result.kind == Isabelle_Process.Kind.STATUS) {
   12.95 -      //{{{ global status message
   12.96 -      message match {
   12.97 -        case XML.Elem(Markup.MESSAGE, _, elems) =>
   12.98 -          for (elem <- elems) {
   12.99 -            elem match {
  12.100 -              // document edits
  12.101 -              case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
  12.102 -                document_versions.find(_.id == doc_id) match {
  12.103 -                  case Some(doc) =>
  12.104 -                    for {
  12.105 -                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
  12.106 -                      <- edits }
  12.107 -                    {
  12.108 -                      commands.get(cmd_id) match {
  12.109 -                        case Some(cmd) =>
  12.110 -                          val state = new Command_State(cmd)
  12.111 -                          states += (state_id -> state)
  12.112 -                          doc.states += (cmd -> state)
  12.113 -                          command_change.event(cmd)   // FIXME really!?
  12.114 -                        case None =>
  12.115 -                      }
  12.116 -                    }
  12.117 -                  case None =>
  12.118 -                }
  12.119 -
  12.120 -              // command and keyword declarations
  12.121 -              case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
  12.122 -                _command_decls += (name -> kind)
  12.123 -                _completion += name
  12.124 -              case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
  12.125 -                _keyword_decls += name
  12.126 -                _completion += name
  12.127 -
  12.128 -              // process ready (after initialization)
  12.129 -              case XML.Elem(Markup.READY, _, _) => prover_ready = true
  12.130 -
  12.131 -              case _ =>
  12.132 -            }
  12.133 -          }
  12.134 -        case _ =>
  12.135 -      }
  12.136 -      //}}}
  12.137 -    }
  12.138 -  }
  12.139 -
  12.140 -
  12.141 -  /* document changes */
  12.142 -
  12.143 -  def begin_document(path: String) {
  12.144 -    process.begin_document(document_0.id, path)
  12.145 -  }
  12.146 -
  12.147 -  def handle_change(change: Change) {
  12.148 -    val old = document(change.parent.get.id).get
  12.149 -    val (doc, changes) = old.text_changed(change)
  12.150 -    document_versions ::= doc
  12.151 -
  12.152 -    val id_changes = changes map { case (c1, c2) =>
  12.153 -        (c1.map(_.id).getOrElse(document_0.id),
  12.154 -         c2 match {
  12.155 -            case None => None
  12.156 -            case Some(command) =>
  12.157 -              commands += (command.id -> command)
  12.158 -              process.define_command(command.id, system.symbols.encode(command.content))
  12.159 -              Some(command.id)
  12.160 -          })
  12.161 -    }
  12.162 -    process.edit_document(old.id, doc.id, id_changes)
  12.163 -
  12.164 -    document_change.event(doc)
  12.165 -  }
  12.166 -
  12.167 -
  12.168 -  /* main controls */
  12.169 -
  12.170 -  def start() { receiver.start() }
  12.171 -
  12.172 -  def stop() { process.kill() }
  12.173 -}
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Tools/jEdit/src/proofdocument/session.scala	Thu Dec 10 22:15:19 2009 +0100
    13.3 @@ -0,0 +1,192 @@
    13.4 +/*
    13.5 + * Isabelle session, potentially with running prover
    13.6 + *
    13.7 + * @author Makarius
    13.8 + */
    13.9 +
   13.10 +package isabelle.proofdocument
   13.11 +
   13.12 +
   13.13 +import scala.actors.Actor._
   13.14 +
   13.15 +
   13.16 +class Session(system: Isabelle_System)
   13.17 +{
   13.18 +  /* main actor */
   13.19 +
   13.20 +  private case class Start(logic: String)
   13.21 +  private case object Stop
   13.22 +
   13.23 +  private var prover: Isabelle_Process with Isar_Document = null
   13.24 +  private var prover_logic = ""
   13.25 +  private var prover_ready = false
   13.26 +
   13.27 +  private val session_actor = actor {
   13.28 +    loop {
   13.29 +      react {
   13.30 +        case Start(logic) =>
   13.31 +          if (prover == null) {
   13.32 +            // FIXME only once
   13.33 +            prover =  // FIXME rebust error handling (via results)
   13.34 +              new Isabelle_Process(system, self,   // FIXME improve options
   13.35 +                  "-m", "xsymbols", "-m", "no_brackets", "-m", "no_type_brackets", logic)
   13.36 +                with Isar_Document
   13.37 +            prover_logic = logic
   13.38 +            reply(())
   13.39 +          }
   13.40 +
   13.41 +        case Stop =>
   13.42 +          if (prover != null)
   13.43 +            prover.kill
   13.44 +          prover = null   // FIXME later (via results)!?
   13.45 +          prover_ready = false // FIXME !??
   13.46 +          
   13.47 +        case change: Change if prover_ready =>
   13.48 +          handle_change(change)
   13.49 +
   13.50 +        case result: Isabelle_Process.Result =>
   13.51 +          handle_result(result)
   13.52 +
   13.53 +        case bad if prover_ready =>
   13.54 +          System.err.println("session_actor: ignoring bad message " + bad)
   13.55 +      }
   13.56 +    }
   13.57 +  }
   13.58 +
   13.59 +  def start(logic: String) { session_actor !? Start(logic) }
   13.60 +  def stop() { session_actor ! Stop }
   13.61 +  def input(change: Change) { session_actor ! change }
   13.62 +
   13.63 +
   13.64 +  /* pervasive event buses */
   13.65 +
   13.66 +  val global_settings = new Event_Bus[Unit]
   13.67 +  val raw_results = new Event_Bus[Isabelle_Process.Result]
   13.68 +  val results = new Event_Bus[Command]
   13.69 +
   13.70 +  val command_change = new Event_Bus[Command]
   13.71 +  val document_change = new Event_Bus[Proof_Document]
   13.72 +
   13.73 +
   13.74 +  /* selected state */  // FIXME!? races!?
   13.75 +
   13.76 +  private var _selected_state: Command = null
   13.77 +  def selected_state = _selected_state
   13.78 +  def selected_state_=(state: Command) { _selected_state = state; results.event(state) }
   13.79 +
   13.80 +
   13.81 +  /* outer syntax keywords and completion */
   13.82 +
   13.83 +  @volatile private var _command_decls = Map[String, String]()
   13.84 +  def command_decls() = _command_decls
   13.85 +
   13.86 +  @volatile private var _keyword_decls = Set[String]()
   13.87 +  def keyword_decls() = _keyword_decls
   13.88 +
   13.89 +  @volatile private var _completion = new Completion + system.symbols
   13.90 +  def completion() = _completion
   13.91 +
   13.92 +
   13.93 +  /* document state information */
   13.94 +
   13.95 +  @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
   13.96 +  @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
   13.97 +  val document_0 =
   13.98 +    Proof_Document.empty.
   13.99 +    set_command_keyword((s: String) => command_decls().contains(s))  // FIXME !?
  13.100 +  @volatile private var document_versions = List(document_0)
  13.101 +
  13.102 +  def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
  13.103 +  def document(id: Isar_Document.Document_ID): Option[Proof_Document] =
  13.104 +    document_versions.find(_.id == id)
  13.105 +
  13.106 +
  13.107 +  /* document changes */
  13.108 +
  13.109 +  def begin_document(path: String)
  13.110 +  {
  13.111 +    prover.begin_document(document_0.id, path)   // FIXME fresh id!?!
  13.112 +  }
  13.113 +
  13.114 +  def handle_change(change: Change)
  13.115 +  {
  13.116 +    val old = document(change.parent.get.id).get
  13.117 +    val (doc, changes) = old.text_changed(change)
  13.118 +    document_versions ::= doc
  13.119 +
  13.120 +    val id_changes = changes map {
  13.121 +      case (c1, c2) =>
  13.122 +        (c1.map(_.id).getOrElse(document_0.id),
  13.123 +         c2 match {
  13.124 +            case None => None
  13.125 +            case Some(command) =>
  13.126 +              commands += (command.id -> command)
  13.127 +              prover.define_command(command.id, system.symbols.encode(command.content))
  13.128 +              Some(command.id)
  13.129 +          })
  13.130 +    }
  13.131 +    prover.edit_document(old.id, doc.id, id_changes)
  13.132 +
  13.133 +    document_change.event(doc)
  13.134 +  }
  13.135 +
  13.136 +
  13.137 +  /* prover results */
  13.138 +
  13.139 +  private def handle_result(result: Isabelle_Process.Result)
  13.140 +  {
  13.141 +    raw_results.event(result)
  13.142 +    val message = Isabelle_Process.parse_message(system, result)
  13.143 +
  13.144 +    val state =
  13.145 +      Position.id_of(result.props) match {
  13.146 +        case None => None
  13.147 +        case Some(id) => commands.get(id) orElse states.get(id) orElse None
  13.148 +      }
  13.149 +    if (state.isDefined) state.get ! (this, message)
  13.150 +    else if (result.kind == Isabelle_Process.Kind.STATUS) {
  13.151 +      //{{{ global status message
  13.152 +      message match {
  13.153 +        case XML.Elem(Markup.MESSAGE, _, elems) =>
  13.154 +          for (elem <- elems) {
  13.155 +            elem match {
  13.156 +              // document edits
  13.157 +              case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
  13.158 +                document_versions.find(_.id == doc_id) match {
  13.159 +                  case Some(doc) =>
  13.160 +                    for {
  13.161 +                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
  13.162 +                      <- edits }
  13.163 +                    {
  13.164 +                      commands.get(cmd_id) match {
  13.165 +                        case Some(cmd) =>
  13.166 +                          val state = new Command_State(cmd)
  13.167 +                          states += (state_id -> state)
  13.168 +                          doc.states += (cmd -> state)
  13.169 +                          command_change.event(cmd)   // FIXME really!?
  13.170 +                        case None =>
  13.171 +                      }
  13.172 +                    }
  13.173 +                  case None =>
  13.174 +                }
  13.175 +
  13.176 +              // command and keyword declarations
  13.177 +              case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
  13.178 +                _command_decls += (name -> kind)
  13.179 +                _completion += name
  13.180 +              case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
  13.181 +                _keyword_decls += name
  13.182 +                _completion += name
  13.183 +
  13.184 +              // process ready (after initialization)
  13.185 +              case XML.Elem(Markup.READY, _, _) => prover_ready = true
  13.186 +
  13.187 +              case _ =>
  13.188 +            }
  13.189 +          }
  13.190 +        case _ =>
  13.191 +      }
  13.192 +      //}}}
  13.193 +    }
  13.194 +  }
  13.195 +}
    14.1 --- a/src/Tools/jEdit/src/proofdocument/state.scala	Thu Dec 10 14:23:28 2009 +0100
    14.2 +++ b/src/Tools/jEdit/src/proofdocument/state.scala	Thu Dec 10 22:15:19 2009 +0100
    14.3 @@ -70,7 +70,7 @@
    14.4  
    14.5    /* message dispatch */
    14.6  
    14.7 -  def + (prover: Prover, message: XML.Tree): State =
    14.8 +  def + (session: Session, message: XML.Tree): State =
    14.9    {
   14.10      val changed: State =
   14.11        message match {
   14.12 @@ -111,7 +111,7 @@
   14.13              })
   14.14          case _ => add_result(message)
   14.15        }
   14.16 -    if (!(this eq changed)) prover.command_change.event(command)
   14.17 +    if (!(this eq changed)) session.command_change.event(command)
   14.18      changed
   14.19    }
   14.20  }
    15.1 --- a/src/Tools/jEdit/src/proofdocument/theory_view.scala	Thu Dec 10 14:23:28 2009 +0100
    15.2 +++ b/src/Tools/jEdit/src/proofdocument/theory_view.scala	Thu Dec 10 22:15:19 2009 +0100
    15.3 @@ -19,7 +19,7 @@
    15.4  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
    15.5  import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
    15.6  
    15.7 -import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker}
    15.8 +import isabelle.jedit.{Document_Overview, Isabelle, Isabelle_Token_Marker}  // FIXME wrong layer
    15.9  
   15.10  
   15.11  object Theory_View
   15.12 @@ -36,16 +36,14 @@
   15.13  }
   15.14  
   15.15  
   15.16 -class Theory_View(text_area: JEditTextArea)
   15.17 +class Theory_View(session: Session, text_area: JEditTextArea)
   15.18  {
   15.19    private val buffer = text_area.getBuffer
   15.20  
   15.21  
   15.22    /* prover setup */
   15.23  
   15.24 -  val prover: Prover = new Prover(Isabelle.system, Isabelle.default_logic())
   15.25 -
   15.26 -  prover.command_change += ((command: Command) =>
   15.27 +  session.command_change += ((command: Command) =>
   15.28      if (current_document().commands.contains(command))
   15.29        Swing_Thread.later {
   15.30          // FIXME proper handling of buffer vs. text areas
   15.31 @@ -60,7 +58,7 @@
   15.32  
   15.33    /* changes vs. edits */
   15.34  
   15.35 -  private val change_0 = new Change(prover.document_0.id, None, Nil)
   15.36 +  private val change_0 = new Change(Isabelle.session.document_0.id, None, Nil)  // FIXME !?
   15.37    private var _changes = List(change_0)   // owned by Swing/AWT thread
   15.38    def changes = _changes
   15.39    private var current_change = change_0
   15.40 @@ -71,7 +69,7 @@
   15.41      if (!edits.isEmpty) {
   15.42        val change = new Change(Isabelle.system.id(), Some(current_change), edits.toList)
   15.43        _changes ::= change
   15.44 -      prover.input(change)
   15.45 +      session.input(change)
   15.46        current_change = change
   15.47        edits.clear
   15.48      }
   15.49 @@ -151,7 +149,7 @@
   15.50  
   15.51    /* activation */
   15.52  
   15.53 -  private val overview = new Document_Overview(prover, text_area, to_current)
   15.54 +  private val overview = new Document_Overview(text_area, to_current)
   15.55  
   15.56    private val selected_state_controller = new CaretListener {
   15.57      override def caretUpdate(e: CaretEvent) {
   15.58 @@ -159,8 +157,8 @@
   15.59        doc.command_at(e.getDot) match {
   15.60          case Some(cmd)
   15.61            if (doc.token_start(cmd.tokens.first) <= e.getDot &&
   15.62 -            Isabelle.plugin.selected_state != cmd) =>
   15.63 -          Isabelle.plugin.selected_state = cmd
   15.64 +            Isabelle.session.selected_state != cmd) =>
   15.65 +          Isabelle.session.selected_state = cmd
   15.66          case _ =>
   15.67        }
   15.68      }
   15.69 @@ -172,7 +170,7 @@
   15.70      text_area.addLeftOfScrollBar(overview)
   15.71      text_area.getPainter.
   15.72        addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
   15.73 -    buffer.setTokenMarker(new Isabelle_Token_Marker(buffer, prover))
   15.74 +    buffer.setTokenMarker(new Isabelle_Token_Marker(buffer))
   15.75      buffer.addBufferListener(buffer_listener)
   15.76      buffer.propertiesChanged()
   15.77    }
   15.78 @@ -190,7 +188,7 @@
   15.79    /* history of changes */
   15.80  
   15.81    private def doc_or_pred(c: Change): Proof_Document =
   15.82 -    prover.document(c.id).getOrElse(doc_or_pred(c.parent.get))
   15.83 +    session.document(c.id).getOrElse(doc_or_pred(c.parent.get))
   15.84  
   15.85    def current_document() = doc_or_pred(current_change)
   15.86  
   15.87 @@ -282,8 +280,8 @@
   15.88      val (start, stop) = lines_of_command(cmd)
   15.89      text_area.invalidateLineRange(start, stop)
   15.90  
   15.91 -    if (Isabelle.plugin.selected_state == cmd)
   15.92 -      Isabelle.plugin.selected_state = cmd  // update State view
   15.93 +    if (Isabelle.session.selected_state == cmd)
   15.94 +      Isabelle.session.selected_state = cmd
   15.95    }
   15.96  
   15.97    private def invalidate_all() =
   15.98 @@ -313,8 +311,6 @@
   15.99  
  15.100    /* init */
  15.101  
  15.102 -  prover.start()
  15.103 -
  15.104    edits += Insert(0, buffer.getText(0, buffer.getLength))
  15.105    edits_delay()
  15.106  }