src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
changeset 34759 bfea7839d9e1
parent 34758 710e3a9a4c95
child 34760 dc7f5e0d9d27
     1.1 --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Tue Dec 08 14:29:29 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,102 +0,0 @@
     1.4 -/*
     1.5 - * SideKick parser for Isabelle proof documents
     1.6 - *
     1.7 - * @author Fabian Immler, TU Munich
     1.8 - * @author Makarius
     1.9 - */
    1.10 -
    1.11 -package isabelle.jedit
    1.12 -
    1.13 -import scala.collection.Set
    1.14 -import scala.collection.immutable.TreeSet
    1.15 -
    1.16 -import javax.swing.tree.DefaultMutableTreeNode
    1.17 -import javax.swing.text.Position
    1.18 -import javax.swing.Icon
    1.19 -
    1.20 -import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
    1.21 -import errorlist.DefaultErrorSource
    1.22 -import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
    1.23 -
    1.24 -import isabelle.prover.{Command, Markup_Node}
    1.25 -import isabelle.proofdocument.ProofDocument
    1.26 -
    1.27 -
    1.28 -class IsabelleSideKickParser extends SideKickParser("isabelle")
    1.29 -{
    1.30 -  /* parsing */
    1.31 -
    1.32 -  @volatile private var stopped = false
    1.33 -  override def stop() = { stopped = true }
    1.34 -
    1.35 -  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    1.36 -  {
    1.37 -    implicit def int_to_pos(offset: Int): Position =
    1.38 -      new Position { def getOffset = offset; override def toString = offset.toString }
    1.39 -
    1.40 -    stopped = false
    1.41 -
    1.42 -    val data = new SideKickParsedData(buffer.getName)
    1.43 -    val root = data.root
    1.44 -    data.getAsset(root).setEnd(buffer.getLength)
    1.45 -
    1.46 -    val prover_setup = Isabelle.prover_setup(buffer)
    1.47 -    if (prover_setup.isDefined) {
    1.48 -      val document = prover_setup.get.theory_view.current_document()
    1.49 -      for (command <- document.commands if !stopped) {
    1.50 -        root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
    1.51 -            {
    1.52 -              val content = command.content(node.start, node.stop)
    1.53 -              val command_start = command.start(document)
    1.54 -              val id = command.id
    1.55 -
    1.56 -              new DefaultMutableTreeNode(new IAsset {
    1.57 -                override def getIcon: Icon = null
    1.58 -                override def getShortString: String = content
    1.59 -                override def getLongString: String = node.info.toString
    1.60 -                override def getName: String = id
    1.61 -                override def setName(name: String) = ()
    1.62 -                override def setStart(start: Position) = ()
    1.63 -                override def getStart: Position = command_start + node.start
    1.64 -                override def setEnd(end: Position) = ()
    1.65 -                override def getEnd: Position = command_start + node.stop
    1.66 -                override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]"
    1.67 -              })
    1.68 -            }))
    1.69 -      }
    1.70 -      if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    1.71 -    }
    1.72 -    else root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    1.73 -
    1.74 -    data
    1.75 -  }
    1.76 -
    1.77 -
    1.78 -  /* completion */
    1.79 -
    1.80 -  override def supportsCompletion = true
    1.81 -  override def canCompleteAnywhere = true
    1.82 -
    1.83 -  override def complete(pane: EditPane, caret: Int): SideKickCompletion =
    1.84 -  {
    1.85 -    val buffer = pane.getBuffer
    1.86 -
    1.87 -    val line = buffer.getLineOfOffset(caret)
    1.88 -    val start = buffer.getLineStartOffset(line)
    1.89 -    val text = buffer.getSegment(start, caret - start)
    1.90 -
    1.91 -    val completion =
    1.92 -      Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion)
    1.93 -
    1.94 -    completion.complete(text) match {
    1.95 -      case None => null
    1.96 -      case Some((word, cs)) =>
    1.97 -        val ds =
    1.98 -          if (Isabelle_Encoding.is_active(buffer))
    1.99 -            cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _)
   1.100 -          else cs
   1.101 -        new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
   1.102 -    }
   1.103 -  }
   1.104 -
   1.105 -}