src/Tools/jEdit/src/isabelle_sidekick.scala
changeset 53274 1760c01f1c78
parent 53233 4b422e5d64fd
child 53281 251e1a2aa792
equal deleted inserted replaced
53273:473ea1ed7503 53274:1760c01f1c78
     8 package isabelle.jedit
     8 package isabelle.jedit
     9 
     9 
    10 
    10 
    11 import isabelle._
    11 import isabelle._
    12 
    12 
    13 import scala.collection.Set
       
    14 import scala.collection.immutable.TreeSet
       
    15 import scala.util.matching.Regex
       
    16 
       
    17 import java.awt.Component
       
    18 import javax.swing.tree.DefaultMutableTreeNode
    13 import javax.swing.tree.DefaultMutableTreeNode
    19 import javax.swing.text.Position
    14 import javax.swing.text.Position
    20 import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList}
    15 import javax.swing.Icon
    21 
    16 
    22 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
    17 import org.gjt.sp.jedit.Buffer
    23 import errorlist.DefaultErrorSource
    18 import sidekick.{SideKickParser, SideKickParsedData, IAsset}
    24 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
       
    25 
    19 
    26 
    20 
    27 object Isabelle_Sidekick
    21 object Isabelle_Sidekick
    28 {
    22 {
    29   def int_to_pos(offset: Text.Offset): Position =
    23   def int_to_pos(offset: Text.Offset): Position =
    56     }
    50     }
    57   }
    51   }
    58 }
    52 }
    59 
    53 
    60 
    54 
    61 class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])
    55 class Isabelle_Sidekick(name: String) extends SideKickParser(name)
    62   extends SideKickParser(name)
    56 {
    63 {
    57   override def supportsCompletion = false
       
    58 
       
    59 
    64   /* parsing */
    60   /* parsing */
    65 
    61 
    66   @volatile protected var stopped = false
    62   @volatile protected var stopped = false
    67   override def stop() = { stopped = true }
    63   override def stop() = { stopped = true }
    68 
    64 
    69   def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
    65   def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
    70 
    66 
    71   def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    67   def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
    72   {
    68   {
    73     stopped = false
    69     stopped = false
    74 
    70 
    75     // FIXME lock buffer (!??)
    71     // FIXME lock buffer (!??)
    76     val data = new SideKickParsedData(buffer.getName)
    72     val data = new SideKickParsedData(buffer.getName)
    77     val root = data.root
    73     val root = data.root
    78     data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
    74     data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
    79 
    75 
    80     val syntax = get_syntax
    76     val syntax = Isabelle.mode_syntax(name)
    81     val ok =
    77     val ok =
    82       if (syntax.isDefined) {
    78       if (syntax.isDefined) {
    83         val ok = parser(buffer, syntax.get, data)
    79         val ok = parser(buffer, syntax.get, data)
    84         if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
    80         if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
    85         else ok
    81         else ok
    87       else false
    83       else false
    88     if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
    84     if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
    89 
    85 
    90     data
    86     data
    91   }
    87   }
    92 
       
    93 
       
    94   /* completion */
       
    95 
       
    96   override def supportsCompletion = true
       
    97   override def canCompleteAnywhere = true
       
    98 
       
    99   override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
       
   100   {
       
   101     Swing_Thread.assert()
       
   102 
       
   103     val buffer = pane.getBuffer
       
   104     JEdit_Lib.buffer_lock(buffer) {
       
   105       get_syntax match {
       
   106         case None => null
       
   107         case Some(syntax) =>
       
   108           val line = buffer.getLineOfOffset(caret)
       
   109           val start = buffer.getLineStartOffset(line)
       
   110           val text = buffer.getSegment(start, caret - start)
       
   111 
       
   112           syntax.completion.complete(text) match {
       
   113             case None => null
       
   114             case Some((word, cs)) =>
       
   115               val ds =
       
   116                 (if (Isabelle_Encoding.is_active(buffer))
       
   117                   cs.map(Symbol.decode(_)).sorted
       
   118                  else cs).filter(_ != word)
       
   119               if (ds.isEmpty) null
       
   120               else
       
   121                 new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) {
       
   122                   override def getRenderer() =
       
   123                     new ListCellRenderer[Any] {
       
   124                       val default_renderer =
       
   125                         (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]]
       
   126 
       
   127                       override def getListCellRendererComponent(
       
   128                           list: JList[_ <: Any], value: Any, index: Int,
       
   129                           selected: Boolean, focus: Boolean): Component =
       
   130                       {
       
   131                         val renderer: Component =
       
   132                           default_renderer.getListCellRendererComponent(
       
   133                             list, value, index, selected, focus)
       
   134                         renderer.setFont(pane.getTextArea.getPainter.getFont)
       
   135                         renderer
       
   136                       }
       
   137                     }
       
   138                 }
       
   139           }
       
   140       }
       
   141     }
       
   142   }
       
   143 }
    88 }
   144 
    89 
   145 
    90 
   146 class Isabelle_Sidekick_Structure(
    91 class Isabelle_Sidekick_Structure(
   147     name: String,
    92     name: String,
   148     get_syntax: => Option[Outer_Syntax],
       
   149     node_name: Buffer => Option[Document.Node.Name])
    93     node_name: Buffer => Option[Document.Node.Name])
   150   extends Isabelle_Sidekick(name, get_syntax)
    94   extends Isabelle_Sidekick(name)
   151 {
    95 {
   152   import Thy_Syntax.Structure
    96   import Thy_Syntax.Structure
   153 
    97 
   154   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
    98   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   155   {
    99   {
   184     }
   128     }
   185   }
   129   }
   186 }
   130 }
   187 
   131 
   188 
   132 
   189 class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
   133 class Isabelle_Sidekick_Default extends
   190   "isabelle", PIDE.get_recent_syntax, PIDE.thy_load.buffer_node_name)
   134   Isabelle_Sidekick_Structure("isabelle", PIDE.thy_load.buffer_node_name)
   191 {
   135 
   192   override def supportsCompletion = false
   136 
   193 }
   137 class Isabelle_Sidekick_Options extends
   194 
   138   Isabelle_Sidekick_Structure("isabelle-options", PIDE.thy_load.buffer_node_dummy)
   195 
   139 
   196 class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
   140 
   197   "isabelle-options", Some(Options.options_syntax), PIDE.thy_load.buffer_node_dummy)
   141 class Isabelle_Sidekick_Root extends
   198 
   142   Isabelle_Sidekick_Structure("isabelle-root", PIDE.thy_load.buffer_node_dummy)
   199 
   143 
   200 class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
   144 
   201   "isabelle-root", Some(Build.root_syntax), PIDE.thy_load.buffer_node_dummy)
   145 class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
   202 
       
   203 
       
   204 class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw", PIDE.get_recent_syntax)
       
   205 {
   146 {
   206   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   147   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   207   {
   148   {
   208     Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
   149     Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
   209       case Some(snapshot) =>
   150       case Some(snapshot) =>
   232     }
   173     }
   233   }
   174   }
   234 }
   175 }
   235 
   176 
   236 
   177 
   237 class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news", Some(Outer_Syntax.empty))
   178 class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
   238 {
   179 {
   239   private val Heading1 = new Regex("""^New in (.*)\w*$""")
   180   private val Heading1 = """^New in (.*)\w*$""".r
   240   private val Heading2 = new Regex("""^\*\*\*\w*(.*)\w*\*\*\*\w*$""")
   181   private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
   241 
   182 
   242   private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
   183   private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
   243     new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop))
   184     new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop))
   244 
   185 
   245   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   186   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   258       offset += line.length + 1
   199       offset += line.length + 1
   259     }
   200     }
   260 
   201 
   261     true
   202     true
   262   }
   203   }
   263 
   204 }
   264   override def supportsCompletion = false
   205 
   265 }
       
   266