wenzelm@43282: /*  Title:      Tools/jEdit/src/isabelle_sidekick.scala
wenzelm@36760:     Author:     Fabian Immler, TU Munich
wenzelm@36760:     Author:     Makarius
wenzelm@36760: 
wenzelm@36760: SideKick parsers for Isabelle proof documents.
wenzelm@36760: */
immler@34393: 
wenzelm@34426: package isabelle.jedit
immler@34393: 
wenzelm@34760: 
wenzelm@36015: import isabelle._
wenzelm@36015: 
immler@34475: import scala.collection.Set
immler@34475: import scala.collection.immutable.TreeSet
wenzelm@34417: 
immler@34393: import javax.swing.tree.DefaultMutableTreeNode
wenzelm@34701: import javax.swing.text.Position
wenzelm@34701: import javax.swing.Icon
wenzelm@34417: 
wenzelm@34609: import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
wenzelm@34417: import errorlist.DefaultErrorSource
wenzelm@34701: import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
wenzelm@34701: 
immler@34393: 
wenzelm@36738: object Isabelle_Sidekick
wenzelm@36738: {
wenzelm@40477:   def int_to_pos(offset: Text.Offset): Position =
wenzelm@36738:     new Position { def getOffset = offset; override def toString = offset.toString }
wenzelm@40452: 
wenzelm@40477:   class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
wenzelm@40452:   {
wenzelm@40452:     protected var _name = name
wenzelm@40452:     protected var _start = int_to_pos(start)
wenzelm@40452:     protected var _end = int_to_pos(end)
wenzelm@40452:     override def getIcon: Icon = null
wenzelm@40452:     override def getShortString: String = _name
wenzelm@40452:     override def getLongString: String = _name
wenzelm@40452:     override def getName: String = _name
wenzelm@40452:     override def setName(name: String) = _name = name
wenzelm@40452:     override def getStart: Position = _start
wenzelm@40452:     override def setStart(start: Position) = _start = start
wenzelm@40452:     override def getEnd: Position = _end
wenzelm@40452:     override def setEnd(end: Position) = _end = end
wenzelm@40452:     override def toString = _name
wenzelm@40452:   }
wenzelm@36738: }
wenzelm@36738: 
wenzelm@36738: 
wenzelm@36759: abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
wenzelm@34625: {
wenzelm@34417:   /* parsing */
wenzelm@34417: 
wenzelm@36759:   @volatile protected var stopped = false
wenzelm@34503:   override def stop() = { stopped = true }
immler@34401: 
wenzelm@36759:   def parser(data: SideKickParsedData, model: Document_Model): Unit
wenzelm@36759: 
wenzelm@34625:   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
wenzelm@34625:   {
wenzelm@34417:     stopped = false
wenzelm@34625: 
wenzelm@38640:     // FIXME lock buffer (!??)
wenzelm@34417:     val data = new SideKickParsedData(buffer.getName)
wenzelm@34717:     val root = data.root
wenzelm@40452:     data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
immler@34475: 
wenzelm@34789:     Swing_Thread.now { Document_Model(buffer) } match {
wenzelm@34784:       case Some(model) =>
wenzelm@36759:         parser(data, model)
wenzelm@34777:         if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
wenzelm@34777:       case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
immler@34475:     }
wenzelm@34417:     data
wenzelm@34417:   }
wenzelm@34417: 
wenzelm@36738: 
wenzelm@34417:   /* completion */
wenzelm@34417: 
wenzelm@34417:   override def supportsCompletion = true
wenzelm@34417:   override def canCompleteAnywhere = true
wenzelm@34417: 
wenzelm@40477:   override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
wenzelm@34609:   {
immler@34475:     val buffer = pane.getBuffer
wenzelm@39624:     Isabelle.swing_buffer_lock(buffer) {
wenzelm@39624:       Document_Model(buffer) match {
wenzelm@39624:         case None => null
wenzelm@39624:         case Some(model) =>
wenzelm@39624:           val line = buffer.getLineOfOffset(caret)
wenzelm@39624:           val start = buffer.getLineStartOffset(line)
wenzelm@39624:           val text = buffer.getSegment(start, caret - start)
immler@34475: 
wenzelm@39624:           val completion = model.session.current_syntax().completion
wenzelm@39624:           completion.complete(text) match {
wenzelm@39624:             case None => null
wenzelm@39624:             case Some((word, cs)) =>
wenzelm@39624:               val ds =
wenzelm@39624:                 (if (Isabelle_Encoding.is_active(buffer))
wenzelm@43661:                   cs.map(Isabelle_System.symbols.decode(_)).sortWith(_ < _)
wenzelm@39624:                  else cs).filter(_ != word)
wenzelm@39624:               if (ds.isEmpty) null
wenzelm@39624:               else new SideKickCompletion(
wenzelm@39624:                 pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
wenzelm@39624:           }
wenzelm@39624:       }
wenzelm@34611:     }
wenzelm@34609:   }
immler@34393: }
wenzelm@36738: 
wenzelm@36738: 
wenzelm@36759: class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
wenzelm@36759: {
wenzelm@40455:   import Thy_Syntax.Structure
wenzelm@40455: 
wenzelm@36759:   def parser(data: SideKickParsedData, model: Document_Model)
wenzelm@36759:   {
wenzelm@40455:     val syntax = model.session.current_syntax()
wenzelm@40455: 
wenzelm@40477:     def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
wenzelm@40455:       entry match {
wenzelm@40455:         case Structure.Block(name, body) =>
wenzelm@40455:           val node =
wenzelm@40455:             new DefaultMutableTreeNode(
wenzelm@40475:               new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
wenzelm@40455:           (offset /: body)((i, e) =>
wenzelm@40455:             {
wenzelm@40455:               make_tree(i, e) foreach (nd => node.add(nd))
wenzelm@40455:               i + e.length
wenzelm@40455:             })
wenzelm@40455:           List(node)
wenzelm@40455:         case Structure.Atom(command)
wenzelm@40458:         if command.is_command && syntax.heading_level(command).isEmpty =>
wenzelm@40455:           val node =
wenzelm@40455:             new DefaultMutableTreeNode(
wenzelm@40455:               new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
wenzelm@40455:           List(node)
wenzelm@40455:         case _ => Nil
wenzelm@40455:       }
wenzelm@40455: 
wenzelm@40474:     val text = Isabelle.buffer_text(model.buffer)
wenzelm@40792:     val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
wenzelm@40455: 
wenzelm@40455:     make_tree(0, structure) foreach (node => data.root.add(node))
wenzelm@36759:   }
wenzelm@36759: }
wenzelm@36738: 
wenzelm@36738: 
wenzelm@36759: class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
wenzelm@36759: {
wenzelm@36759:   def parser(data: SideKickParsedData, model: Document_Model)
wenzelm@36759:   {
wenzelm@36759:     val root = data.root
wenzelm@38223:     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
wenzelm@38569:     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
wenzelm@38658:       snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
wenzelm@36759:           {
wenzelm@38663:             val range = info.range + command_start
wenzelm@38577:             val content = command.source(info.range).replace('\n', ' ')
wenzelm@38663:             val info_text =
wenzelm@38663:               info.info match {
wenzelm@38663:                 case elem @ XML.Elem(_, _) =>
wenzelm@38663:                   Pretty.formatted(List(elem), margin = 40).mkString("\n")
wenzelm@38663:                 case x => x.toString
wenzelm@38663:               }
wenzelm@36738: 
wenzelm@40452:             new DefaultMutableTreeNode(
wenzelm@40452:               new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
wenzelm@40452:                 override def getShortString: String = content
wenzelm@40452:                 override def getLongString: String = info_text
wenzelm@40452:                 override def toString = "\"" + content + "\" " + range.toString
wenzelm@40452:               })
wenzelm@38479:           })
wenzelm@36759:     }
wenzelm@36759:   }
wenzelm@36759: }
wenzelm@36738: