src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 56814 eb8f2a5a57ad
child 57900 fd03765b06c0
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     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 javax.swing.tree.DefaultMutableTreeNode
    14 import javax.swing.text.Position
    15 import javax.swing.Icon
    16 
    17 import org.gjt.sp.jedit.Buffer
    18 import sidekick.{SideKickParser, SideKickParsedData, IAsset}
    19 
    20 
    21 object Isabelle_Sidekick
    22 {
    23   def int_to_pos(offset: Text.Offset): Position =
    24     new Position { def getOffset = offset; override def toString = offset.toString }
    25 
    26   class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
    27   {
    28     protected var _name = name
    29     protected var _start = int_to_pos(start)
    30     protected var _end = int_to_pos(end)
    31     override def getIcon: Icon = null
    32     override def getShortString: String =
    33       "<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" +
    34       HTML.encode(_name) + "</span></html>"
    35     override def getLongString: String = _name
    36     override def getName: String = _name
    37     override def setName(name: String) = _name = name
    38     override def getStart: Position = _start
    39     override def setStart(start: Position) = _start = start
    40     override def getEnd: Position = _end
    41     override def setEnd(end: Position) = _end = end
    42     override def toString = _name
    43   }
    44 
    45   def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
    46     swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
    47   {
    48     for ((_, entry) <- tree.branches) {
    49       val node = swing_node(Text.Info(entry.range, entry.markup))
    50       swing_markup_tree(entry.subtree, node, swing_node)
    51       parent.add(node)
    52     }
    53   }
    54 }
    55 
    56 
    57 class Isabelle_Sidekick(name: String) extends SideKickParser(name)
    58 {
    59   override def supportsCompletion = false
    60 
    61 
    62   /* parsing */
    63 
    64   @volatile protected var stopped = false
    65   override def stop() = { stopped = true }
    66 
    67   def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
    68 
    69   def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
    70   {
    71     stopped = false
    72 
    73     // FIXME lock buffer (!??)
    74     val data = new SideKickParsedData(buffer.getName)
    75     val root = data.root
    76     data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
    77 
    78     val syntax = Isabelle.mode_syntax(name)
    79     val ok =
    80       if (syntax.isDefined) {
    81         val ok = parser(buffer, syntax.get, data)
    82         if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
    83         else ok
    84       }
    85       else false
    86     if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
    87 
    88     data
    89   }
    90 }
    91 
    92 
    93 class Isabelle_Sidekick_Structure(
    94     name: String,
    95     node_name: Buffer => Option[Document.Node.Name])
    96   extends Isabelle_Sidekick(name)
    97 {
    98   import Thy_Syntax.Structure
    99 
   100   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   101   {
   102     def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
   103       entry match {
   104         case Structure.Block(name, body) =>
   105           val node =
   106             new DefaultMutableTreeNode(
   107               new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
   108           (offset /: body)((i, e) =>
   109             {
   110               make_tree(i, e) foreach (nd => node.add(nd))
   111               i + e.length
   112             })
   113           List(node)
   114         case Structure.Atom(command)
   115         if command.is_command && syntax.heading_level(command).isEmpty =>
   116           val node =
   117             new DefaultMutableTreeNode(
   118               new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
   119           List(node)
   120         case _ => Nil
   121       }
   122 
   123     node_name(buffer) match {
   124       case Some(name) =>
   125         val text = JEdit_Lib.buffer_text(buffer)
   126         val structure = Structure.parse(syntax, name, text)
   127         make_tree(0, structure) foreach (node => data.root.add(node))
   128         true
   129       case None => false
   130     }
   131   }
   132 }
   133 
   134 
   135 class Isabelle_Sidekick_Default extends
   136   Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name)
   137 
   138 
   139 class Isabelle_Sidekick_Options extends
   140   Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")))
   141 
   142 
   143 class Isabelle_Sidekick_Root extends
   144   Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")))
   145 
   146 
   147 class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
   148 {
   149   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   150   {
   151     val opt_snapshot =
   152       GUI_Thread.now {
   153         Document_Model(buffer) match {
   154           case Some(model) if model.is_theory => Some(model.snapshot)
   155           case _ => None
   156         }
   157       }
   158     opt_snapshot match {
   159       case Some(snapshot) =>
   160         val root = data.root
   161         for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
   162           val markup =
   163             snapshot.state.command_markup(
   164               snapshot.version, command, Command.Markup_Index.markup,
   165                 command.range, Markup.Elements.full)
   166           Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
   167               {
   168                 val range = info.range + command_start
   169                 val content = command.source(info.range).replace('\n', ' ')
   170                 val info_text =
   171                   Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)
   172                     .mkString
   173 
   174                 new DefaultMutableTreeNode(
   175                   new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
   176                     override def getShortString: String = content
   177                     override def getLongString: String = info_text
   178                     override def toString = quote(content) + " " + range.toString
   179                   })
   180               })
   181         }
   182         true
   183       case None => false
   184     }
   185   }
   186 }
   187 
   188 
   189 class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
   190 {
   191   private val Heading1 = """^New in (.*)\w*$""".r
   192   private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
   193 
   194   private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
   195     new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop))
   196 
   197   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   198   {
   199     var offset = 0
   200 
   201     for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
   202       line match {
   203         case Heading1(s) =>
   204           data.root.add(make_node(s, offset, offset + line.length))
   205         case Heading2(s) =>
   206           data.root.getLastChild.asInstanceOf[DefaultMutableTreeNode]
   207             .add(make_node(s, offset, offset + line.length))
   208         case _ =>
   209       }
   210       offset += line.length + 1
   211     }
   212 
   213     true
   214   }
   215 }
   216