src/Tools/jEdit/src/isabelle_sidekick.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64813 7283f41d05ab
child 65130 695930882487
permissions -rw-r--r--
tuned signature;
     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.{JLabel, 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: String = offset.toString }
    25 
    26   def root_data(buffer: Buffer): SideKickParsedData =
    27   {
    28     val data = new SideKickParsedData(buffer.getName)
    29     data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength))
    30     data
    31   }
    32 
    33   class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
    34   {
    35     private val css = GUI.imitate_font_css((new JLabel).getFont, Font_Info.main_family())
    36 
    37     protected var _name = text
    38     protected var _start = int_to_pos(range.start)
    39     protected var _end = int_to_pos(range.stop)
    40     override def getIcon: Icon = null
    41     override def getShortString: String =
    42     {
    43       val n = keyword.length
    44       val s =
    45         _name.indexOf(keyword) match {
    46           case i if i >= 0 && n > 0 =>
    47             HTML.output(_name.substring(0, i)) +
    48             "<b>" + HTML.output(keyword) + "</b>" +
    49             HTML.output(_name.substring(i + n))
    50           case _ => HTML.output(_name)
    51         }
    52       "<html><span style=\"" + css + "\">" + s + "</span></html>"
    53     }
    54     override def getLongString: String = _name
    55     override def getName: String = _name
    56     override def setName(name: String) = _name = name
    57     override def getStart: Position = _start
    58     override def setStart(start: Position) = _start = start
    59     override def getEnd: Position = _end
    60     override def setEnd(end: Position) = _end = end
    61     override def toString: String = _name
    62   }
    63 
    64   class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
    65 
    66   def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
    67     swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
    68   {
    69     for ((_, entry) <- tree.branches) {
    70       val node = swing_node(Text.Info(entry.range, entry.markup))
    71       swing_markup_tree(entry.subtree, node, swing_node)
    72       parent.add(node)
    73     }
    74   }
    75 }
    76 
    77 
    78 class Isabelle_Sidekick(name: String) extends SideKickParser(name)
    79 {
    80   override def supportsCompletion = false
    81 
    82 
    83   /* parsing */
    84 
    85   @volatile protected var stopped = false
    86   override def stop() = { stopped = true }
    87 
    88   def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
    89 
    90   def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
    91   {
    92     stopped = false
    93 
    94     // FIXME lock buffer (!??)
    95     val data = Isabelle_Sidekick.root_data(buffer)
    96     val syntax = Isabelle.buffer_syntax(buffer)
    97     val ok =
    98       if (syntax.isDefined) {
    99         val ok = parser(buffer, syntax.get, data)
   100         if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true }
   101         else ok
   102       }
   103       else false
   104     if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>"))
   105 
   106     data
   107   }
   108 }
   109 
   110 
   111 class Isabelle_Sidekick_Structure(
   112     name: String,
   113     node_name: Buffer => Option[Document.Node.Name],
   114     parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document])
   115   extends Isabelle_Sidekick(name)
   116 {
   117   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   118   {
   119     def make_tree(
   120       parent: DefaultMutableTreeNode,
   121       offset: Text.Offset,
   122       documents: List[Document_Structure.Document])
   123     {
   124       (offset /: documents) { case (i, document) =>
   125         document match {
   126           case Document_Structure.Block(name, text, body) =>
   127             val range = Text.Range(i, i + document.length)
   128             val node =
   129               new DefaultMutableTreeNode(
   130                 new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
   131             parent.add(node)
   132             make_tree(node, i, body)
   133           case _ =>
   134         }
   135         i + document.length
   136       }
   137     }
   138 
   139     node_name(buffer) match {
   140       case Some(name) =>
   141         make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
   142         true
   143       case None =>
   144         false
   145     }
   146   }
   147 }
   148 
   149 class Isabelle_Sidekick_Default extends
   150   Isabelle_Sidekick_Structure("isabelle",
   151     PIDE.resources.theory_node_name, Document_Structure.parse_sections _)
   152 
   153 class Isabelle_Sidekick_Context extends
   154   Isabelle_Sidekick_Structure("isabelle-context",
   155     PIDE.resources.theory_node_name, Document_Structure.parse_blocks _)
   156 
   157 class Isabelle_Sidekick_Options extends
   158   Isabelle_Sidekick_Structure("isabelle-options",
   159     _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections _)
   160 
   161 class Isabelle_Sidekick_Root extends
   162   Isabelle_Sidekick_Structure("isabelle-root",
   163     _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections _)
   164 
   165 class Isabelle_Sidekick_ML extends
   166   Isabelle_Sidekick_Structure("isabelle-ml",
   167     buffer => Some(PIDE.resources.node_name(buffer)),
   168     (_, _, text) => Document_Structure.parse_ml_sections(false, text))
   169 
   170 class Isabelle_Sidekick_SML extends
   171   Isabelle_Sidekick_Structure("isabelle-sml",
   172     buffer => Some(PIDE.resources.node_name(buffer)),
   173     (_, _, text) => Document_Structure.parse_ml_sections(true, text))
   174 
   175 
   176 class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
   177 {
   178   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   179   {
   180     val opt_snapshot =
   181       Document_Model.get(buffer) match {
   182         case Some(model) if model.is_theory => Some(model.snapshot)
   183         case _ => None
   184       }
   185     opt_snapshot match {
   186       case Some(snapshot) =>
   187         for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
   188           val markup =
   189             snapshot.state.command_markup(
   190               snapshot.version, command, Command.Markup_Index.markup,
   191                 command.range, Markup.Elements.full)
   192           Isabelle_Sidekick.swing_markup_tree(markup, data.root,
   193             (info: Text.Info[List[XML.Elem]]) =>
   194               {
   195                 val range = info.range + command_start
   196                 val content = command.source(info.range).replace('\n', ' ')
   197                 val info_text =
   198                   Pretty.formatted(Library.separate(Pretty.fbrk, info.info), margin = 40.0)
   199                     .mkString
   200 
   201                 new DefaultMutableTreeNode(
   202                   new Isabelle_Sidekick.Asset(command.toString, range) {
   203                     override def getShortString: String = content
   204                     override def getLongString: String = info_text
   205                     override def toString: String = quote(content) + " " + range.toString
   206                   })
   207               })
   208         }
   209         true
   210       case None => false
   211     }
   212   }
   213 }
   214 
   215 
   216 class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
   217 {
   218   private val Heading1 = """^New in (.*)\w*$""".r
   219   private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
   220 
   221   private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
   222     new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop)))
   223 
   224   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   225   {
   226     var offset = 0
   227     var end_offset = 0
   228 
   229     var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
   230     var start2: Option[(Int, String)] = None
   231 
   232     def close1: Unit =
   233       start1 match {
   234         case Some((start_offset, s, body)) =>
   235           val node = make_node(s, start_offset, end_offset)
   236           body.foreach(node.add(_))
   237           data.root.add(node)
   238           start1 = None
   239         case None =>
   240       }
   241 
   242     def close2: Unit =
   243       start2 match {
   244         case Some((start_offset, s)) =>
   245           start1 match {
   246             case Some((start_offset1, s1, body)) =>
   247               val node = make_node(s, start_offset, end_offset)
   248               start1 = Some((start_offset1, s1, body :+ node))
   249             case None =>
   250           }
   251           start2 = None
   252         case None =>
   253       }
   254 
   255     for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
   256       line match {
   257         case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector()))
   258         case Heading2(s) => close2; start2 = Some((offset, s))
   259         case _ =>
   260       }
   261       offset += line.length + 1
   262       if (!line.forall(Character.isSpaceChar(_))) end_offset = offset
   263     }
   264     if (!stopped) { close2; close1 }
   265 
   266     true
   267   }
   268 }
   269