src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Thu Mar 15 11:37:56 2012 +0100 (2012-03-15)
changeset 46941 c0f776b661fa
parent 46920 5f44c8bea84e
child 47539 436ae5ea4f80
permissions -rw-r--r--
maintain Version.syntax within document state;
clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;
     1 /*  Title:      Tools/jEdit/src/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   def int_to_pos(offset: Text.Offset): Position =
    28     new Position { def getOffset = offset; override def toString = offset.toString }
    29 
    30   class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
    31   {
    32     protected var _name = name
    33     protected var _start = int_to_pos(start)
    34     protected var _end = int_to_pos(end)
    35     override def getIcon: Icon = null
    36     override def getShortString: String = _name
    37     override def getLongString: String = _name
    38     override def getName: String = _name
    39     override def setName(name: String) = _name = name
    40     override def getStart: Position = _start
    41     override def setStart(start: Position) = _start = start
    42     override def getEnd: Position = _end
    43     override def setEnd(end: Position) = _end = end
    44     override def toString = _name
    45   }
    46 }
    47 
    48 
    49 abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
    50 {
    51   /* parsing */
    52 
    53   @volatile protected var stopped = false
    54   override def stop() = { stopped = true }
    55 
    56   def parser(data: SideKickParsedData, model: Document_Model): Unit
    57 
    58   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    59   {
    60     stopped = false
    61 
    62     // FIXME lock buffer (!??)
    63     val data = new SideKickParsedData(buffer.getName)
    64     val root = data.root
    65     data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
    66 
    67     Swing_Thread.now { Document_Model(buffer) } match {
    68       case Some(model) =>
    69         parser(data, model)
    70         if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    71       case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    72     }
    73     data
    74   }
    75 
    76 
    77   /* completion */
    78 
    79   override def supportsCompletion = true
    80   override def canCompleteAnywhere = true
    81 
    82   override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
    83   {
    84     Swing_Thread.assert()
    85 
    86     val buffer = pane.getBuffer
    87     Isabelle.buffer_lock(buffer) {
    88       Document_Model(buffer) match {
    89         case None => null
    90         case Some(model) =>
    91           val line = buffer.getLineOfOffset(caret)
    92           val start = buffer.getLineStartOffset(line)
    93           val text = buffer.getSegment(start, caret - start)
    94 
    95           val completion = model.session.recent_syntax().completion
    96           completion.complete(text) match {
    97             case None => null
    98             case Some((word, cs)) =>
    99               val ds =
   100                 (if (Isabelle_Encoding.is_active(buffer))
   101                   cs.map(Symbol.decode(_)).sorted
   102                  else cs).filter(_ != word)
   103               if (ds.isEmpty) null
   104               else new SideKickCompletion(
   105                 pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
   106           }
   107       }
   108     }
   109   }
   110 }
   111 
   112 
   113 class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
   114 {
   115   import Thy_Syntax.Structure
   116 
   117   def parser(data: SideKickParsedData, model: Document_Model)
   118   {
   119     val syntax = model.session.recent_syntax()
   120 
   121     def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
   122       entry match {
   123         case Structure.Block(name, body) =>
   124           val node =
   125             new DefaultMutableTreeNode(
   126               new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
   127           (offset /: body)((i, e) =>
   128             {
   129               make_tree(i, e) foreach (nd => node.add(nd))
   130               i + e.length
   131             })
   132           List(node)
   133         case Structure.Atom(command)
   134         if command.is_command && syntax.heading_level(command).isEmpty =>
   135           val node =
   136             new DefaultMutableTreeNode(
   137               new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
   138           List(node)
   139         case _ => Nil
   140       }
   141 
   142     val text = Isabelle.buffer_text(model.buffer)
   143     val structure = Structure.parse(syntax, model.name, text)
   144 
   145     make_tree(0, structure) foreach (node => data.root.add(node))
   146   }
   147 }
   148 
   149 
   150 class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
   151 {
   152   def parser(data: SideKickParsedData, model: Document_Model)
   153   {
   154     val root = data.root
   155     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
   156     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
   157       snapshot.state.command_state(snapshot.version, command).markup
   158         .swing_tree(root)((info: Text.Markup) =>
   159           {
   160             val range = info.range + command_start
   161             val content = command.source(info.range).replace('\n', ' ')
   162             val info_text =
   163               info.info match {
   164                 case elem @ XML.Elem(_, _) => Pretty.formatted(List(elem), margin = 40).mkString
   165                 case x => x.toString
   166               }
   167 
   168             new DefaultMutableTreeNode(
   169               new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
   170                 override def getShortString: String = content
   171                 override def getLongString: String = info_text
   172                 override def toString = quote(content) + " " + range.toString
   173               })
   174           })
   175     }
   176   }
   177 }
   178