tuned signature;
authorwenzelm
Mon Dec 01 17:43:23 2014 +0100 (2014-12-01)
changeset 590747836d927ffca
parent 59073 dcecfcc56dce
child 59075 9f87eb298b75
tuned signature;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/structure_matching.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Dec 01 15:21:49 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Dec 01 17:43:23 2014 +0100
     1.3 @@ -157,7 +157,7 @@
     1.4        val buffer = text_area.getBuffer
     1.5        val decode = Isabelle_Encoding.is_active(buffer)
     1.6  
     1.7 -      Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
     1.8 +      Isabelle.buffer_syntax(buffer) match {
     1.9          case Some(syntax) =>
    1.10            val context =
    1.11              (for {
     2.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Dec 01 15:21:49 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Dec 01 17:43:23 2014 +0100
     2.3 @@ -15,6 +15,7 @@
     2.4  import scala.swing.event.ButtonClicked
     2.5  
     2.6  import org.gjt.sp.jedit.{jEdit, View, Buffer}
     2.7 +import org.gjt.sp.jedit.buffer.JEditBuffer
     2.8  import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher}
     2.9  import org.gjt.sp.jedit.syntax.TokenMarker
    2.10  import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
    2.11 @@ -65,6 +66,9 @@
    2.12        case _ => None
    2.13      }
    2.14  
    2.15 +  def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
    2.16 +    mode_syntax(JEdit_Lib.buffer_mode(buffer))
    2.17 +
    2.18  
    2.19    /* token markers */
    2.20  
     3.1 --- a/src/Tools/jEdit/src/structure_matching.scala	Mon Dec 01 15:21:49 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/structure_matching.scala	Mon Dec 01 17:43:23 2014 +0100
     3.3 @@ -40,7 +40,7 @@
     3.4        val caret_line = text_area.getCaretLine
     3.5        val caret = text_area.getCaretPosition
     3.6  
     3.7 -      Isabelle.session_syntax() match {
     3.8 +      Isabelle.buffer_syntax(text_area.getBuffer) match {
     3.9          case Some(syntax) =>
    3.10            val limit = PIDE.options.value.int("jedit_structure_limit") max 0
    3.11  
    3.12 @@ -143,7 +143,7 @@
    3.13      {
    3.14        def get_span(offset: Text.Offset): Option[Text.Range] =
    3.15          for {
    3.16 -          syntax <- Isabelle.session_syntax()
    3.17 +          syntax <- Isabelle.buffer_syntax(text_area.getBuffer)
    3.18            span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
    3.19          } yield span.range
    3.20