src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34777 91d6089cef88
permissions -rw-r--r--
misc modernization of names;
     1 /*
     2  * SideKick parser for Isabelle proof documents
     3  *
     4  * @author Fabian Immler, TU Munich
     5  * @author Makarius
     6  */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import scala.collection.Set
    12 import scala.collection.immutable.TreeSet
    13 
    14 import javax.swing.tree.DefaultMutableTreeNode
    15 import javax.swing.text.Position
    16 import javax.swing.Icon
    17 
    18 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
    19 import errorlist.DefaultErrorSource
    20 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
    21 
    22 import isabelle.proofdocument.{Command, Markup_Node, Proof_Document}
    23 
    24 
    25 class Isabelle_Sidekick extends SideKickParser("isabelle")
    26 {
    27   /* parsing */
    28 
    29   @volatile private var stopped = false
    30   override def stop() = { stopped = true }
    31 
    32   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    33   {
    34     implicit def int_to_pos(offset: Int): Position =
    35       new Position { def getOffset = offset; override def toString = offset.toString }
    36 
    37     stopped = false
    38 
    39     val data = new SideKickParsedData(buffer.getName)
    40     val root = data.root
    41     data.getAsset(root).setEnd(buffer.getLength)
    42 
    43     val prover_setup = Isabelle.prover_setup(buffer)
    44     if (prover_setup.isDefined) {
    45       val document = prover_setup.get.theory_view.current_document()
    46       for (command <- document.commands if !stopped) {
    47         root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
    48             {
    49               val content = command.content(node.start, node.stop)
    50               val command_start = command.start(document)
    51               val id = command.id
    52 
    53               new DefaultMutableTreeNode(new IAsset {
    54                 override def getIcon: Icon = null
    55                 override def getShortString: String = content
    56                 override def getLongString: String = node.info.toString
    57                 override def getName: String = id
    58                 override def setName(name: String) = ()
    59                 override def setStart(start: Position) = ()
    60                 override def getStart: Position = command_start + node.start
    61                 override def setEnd(end: Position) = ()
    62                 override def getEnd: Position = command_start + node.stop
    63                 override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    64               })
    65             }))
    66       }
    67       if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    68     }
    69     else root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    70 
    71     data
    72   }
    73 
    74 
    75   /* completion */
    76 
    77   override def supportsCompletion = true
    78   override def canCompleteAnywhere = true
    79 
    80   override def complete(pane: EditPane, caret: Int): SideKickCompletion =
    81   {
    82     val buffer = pane.getBuffer
    83 
    84     val line = buffer.getLineOfOffset(caret)
    85     val start = buffer.getLineStartOffset(line)
    86     val text = buffer.getSegment(start, caret - start)
    87 
    88     val completion =
    89       Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion)
    90 
    91     completion.complete(text) match {
    92       case None => null
    93       case Some((word, cs)) =>
    94         val ds =
    95           if (Isabelle_Encoding.is_active(buffer))
    96             cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _)
    97           else cs
    98         new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
    99     }
   100   }
   101 
   102 }