src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
author wenzelm
Sun Aug 15 14:18:52 2010 +0200 (2010-08-15)
changeset 38417 b8922ae21111
parent 38414 49f1f657adc2
child 38426 2858ec7b6dd8
permissions -rw-r--r--
renamed class Document to Document.Version etc.;
renamed Change.prev to Change.previous, and Change.document to Change.current;
tuned;
     1 /*  Title:      Tools/jEdit/src/jedit/isabelle_sidekick.scala
     2     Author:     Fabian Immler, TU Munich
     3     Author:     Makarius
     4 
     5 SideKick parsers for Isabelle proof documents.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import scala.collection.Set
    14 import scala.collection.immutable.TreeSet
    15 
    16 import javax.swing.tree.DefaultMutableTreeNode
    17 import javax.swing.text.Position
    18 import javax.swing.Icon
    19 
    20 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
    21 import errorlist.DefaultErrorSource
    22 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
    23 
    24 
    25 object Isabelle_Sidekick
    26 {
    27   implicit def int_to_pos(offset: Int): Position =
    28     new Position { def getOffset = offset; override def toString = offset.toString }
    29 }
    30 
    31 
    32 abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
    33 {
    34   /* parsing */
    35 
    36   @volatile protected var stopped = false
    37   override def stop() = { stopped = true }
    38 
    39   def parser(data: SideKickParsedData, model: Document_Model): Unit
    40 
    41   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    42   {
    43     import Isabelle_Sidekick.int_to_pos
    44 
    45     stopped = false
    46 
    47     // FIXME lock buffer !??
    48     val data = new SideKickParsedData(buffer.getName)
    49     val root = data.root
    50     data.getAsset(root).setEnd(buffer.getLength)
    51 
    52     Swing_Thread.now { Document_Model(buffer) } match {
    53       case Some(model) =>
    54         parser(data, model)
    55         if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    56       case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    57     }
    58     data
    59   }
    60 
    61 
    62   /* completion */
    63 
    64   override def supportsCompletion = true
    65   override def canCompleteAnywhere = true
    66 
    67   override def complete(pane: EditPane, caret: Int): SideKickCompletion =
    68   {
    69     val buffer = pane.getBuffer
    70 
    71     val line = buffer.getLineOfOffset(caret)
    72     val start = buffer.getLineStartOffset(line)
    73     val text = buffer.getSegment(start, caret - start)
    74 
    75     val completion = Isabelle.session.current_syntax.completion
    76 
    77     completion.complete(text) match {
    78       case None => null
    79       case Some((word, cs)) =>
    80         val ds =
    81           (if (Isabelle_Encoding.is_active(buffer))
    82             cs.map(Isabelle.system.symbols.decode(_)).sort(_ < _)
    83            else cs).filter(_ != word)
    84         if (ds.isEmpty) null
    85         else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
    86     }
    87   }
    88 }
    89 
    90 
    91 class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
    92 {
    93   def parser(data: SideKickParsedData, model: Document_Model)
    94   {
    95     import Isabelle_Sidekick.int_to_pos
    96 
    97     val root = data.root
    98     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
    99     for {
   100       (command, command_start) <- snapshot.node.command_range(0)
   101       if command.is_command && !stopped
   102     }
   103     {
   104       val name = command.name
   105       val node =
   106         new DefaultMutableTreeNode(new IAsset {
   107           override def getIcon: Icon = null
   108           override def getShortString: String = name
   109           override def getLongString: String = name
   110           override def getName: String = name
   111           override def setName(name: String) = ()
   112           override def setStart(start: Position) = ()
   113           override def getStart: Position = command_start
   114           override def setEnd(end: Position) = ()
   115           override def getEnd: Position = command_start + command.length
   116           override def toString = name})
   117       root.add(node)
   118     }
   119   }
   120 }
   121 
   122 
   123 class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
   124 {
   125   def parser(data: SideKickParsedData, model: Document_Model)
   126   {
   127     import Isabelle_Sidekick.int_to_pos
   128 
   129     val root = data.root
   130     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
   131     for ((command, command_start) <- snapshot.node.command_range(0) if !stopped) {
   132       root.add(snapshot.state(command).markup.swing_tree((node: Markup_Node) =>
   133           {
   134             val content = command.source(node.start, node.stop).replace('\n', ' ')
   135             val id = command.id
   136 
   137             new DefaultMutableTreeNode(new IAsset {
   138               override def getIcon: Icon = null
   139               override def getShortString: String = content
   140               override def getLongString: String = node.info.toString
   141               override def getName: String = Markup.Long(id)
   142               override def setName(name: String) = ()
   143               override def setStart(start: Position) = ()
   144               override def getStart: Position = command_start + node.start
   145               override def setEnd(end: Position) = ()
   146               override def getEnd: Position = command_start + node.stop
   147               override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
   148             })
   149           }))
   150     }
   151   }
   152 }
   153