src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Thu Jul 07 13:48:30 2011 +0200 (2011-07-07)
changeset 43695 5130dfe1b7be
parent 43661 39fdbd814c7f
child 44181 bbce0417236d
permissions -rw-r--r--
simplified Symbol based on lazy Symbol.Interpretation -- reduced odd "functorial style";
tuned implicit build/init messages;
     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     val buffer = pane.getBuffer
    85     Isabelle.swing_buffer_lock(buffer) {
    86       Document_Model(buffer) match {
    87         case None => null
    88         case Some(model) =>
    89           val line = buffer.getLineOfOffset(caret)
    90           val start = buffer.getLineStartOffset(line)
    91           val text = buffer.getSegment(start, caret - start)
    92 
    93           val completion = model.session.current_syntax().completion
    94           completion.complete(text) match {
    95             case None => null
    96             case Some((word, cs)) =>
    97               val ds =
    98                 (if (Isabelle_Encoding.is_active(buffer))
    99                   cs.map(Symbol.decode(_)).sortWith(_ < _)
   100                  else cs).filter(_ != word)
   101               if (ds.isEmpty) null
   102               else new SideKickCompletion(
   103                 pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
   104           }
   105       }
   106     }
   107   }
   108 }
   109 
   110 
   111 class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
   112 {
   113   import Thy_Syntax.Structure
   114 
   115   def parser(data: SideKickParsedData, model: Document_Model)
   116   {
   117     val syntax = model.session.current_syntax()
   118 
   119     def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
   120       entry match {
   121         case Structure.Block(name, body) =>
   122           val node =
   123             new DefaultMutableTreeNode(
   124               new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
   125           (offset /: body)((i, e) =>
   126             {
   127               make_tree(i, e) foreach (nd => node.add(nd))
   128               i + e.length
   129             })
   130           List(node)
   131         case Structure.Atom(command)
   132         if command.is_command && syntax.heading_level(command).isEmpty =>
   133           val node =
   134             new DefaultMutableTreeNode(
   135               new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
   136           List(node)
   137         case _ => Nil
   138       }
   139 
   140     val text = Isabelle.buffer_text(model.buffer)
   141     val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
   142 
   143     make_tree(0, structure) foreach (node => data.root.add(node))
   144   }
   145 }
   146 
   147 
   148 class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
   149 {
   150   def parser(data: SideKickParsedData, model: Document_Model)
   151   {
   152     val root = data.root
   153     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
   154     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
   155       snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
   156           {
   157             val range = info.range + command_start
   158             val content = command.source(info.range).replace('\n', ' ')
   159             val info_text =
   160               info.info match {
   161                 case elem @ XML.Elem(_, _) =>
   162                   Pretty.formatted(List(elem), margin = 40).mkString("\n")
   163                 case x => x.toString
   164               }
   165 
   166             new DefaultMutableTreeNode(
   167               new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
   168                 override def getShortString: String = content
   169                 override def getLongString: String = info_text
   170                 override def toString = "\"" + content + "\" " + range.toString
   171               })
   172           })
   173     }
   174   }
   175 }
   176