clarified Sidekick configuration, including minor modes;
authorwenzelm
Tue Aug 07 21:38:24 2012 +0200 (2012-08-07)
changeset 48717622251b2b0f1
parent 48713 de26cf3191a3
child 48718 73e6c22e2d94
clarified Sidekick configuration, including minor modes;
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/services.xml
     1.1 --- a/src/Tools/jEdit/src/Isabelle.props	Tue Aug 07 20:28:35 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Tue Aug 07 21:38:24 2012 +0200
     1.3 @@ -67,9 +67,15 @@
     1.4  isabelle-syslog.title=Syslog
     1.5  
     1.6  #SideKick
     1.7 +mode.isabelle.sidekick.showStatusWindow.label=true
     1.8  sidekick.parser.isabelle.label=Isabelle
     1.9  mode.isabelle.sidekick.parser=isabelle
    1.10 +mode.isabelle-options.sidekick.parser=isabelle-options
    1.11 +mode.isabelle-root.sidekick.parser=isabelle-root
    1.12  mode.ml.sidekick.parser=isabelle
    1.13  
    1.14 +mode.isabelle.customSettings=true
    1.15 +mode.isabelle.folding=sidekick
    1.16 +
    1.17  #Hyperlinks
    1.18  mode.isabelle.hyperlink.source=isabelle
     2.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 07 20:28:35 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 07 21:38:24 2012 +0200
     2.3 @@ -48,14 +48,15 @@
     2.4  }
     2.5  
     2.6  
     2.7 -abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
     2.8 +class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])
     2.9 +  extends SideKickParser(name)
    2.10  {
    2.11    /* parsing */
    2.12  
    2.13    @volatile protected var stopped = false
    2.14    override def stop() = { stopped = true }
    2.15  
    2.16 -  def parser(data: SideKickParsedData, model: Document_Model): Unit
    2.17 +  def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
    2.18  
    2.19    def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
    2.20    {
    2.21 @@ -66,12 +67,16 @@
    2.22      val root = data.root
    2.23      data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
    2.24  
    2.25 -    Swing_Thread.now { Document_Model(buffer) } match {
    2.26 -      case Some(model) =>
    2.27 -        parser(data, model)
    2.28 -        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
    2.29 -      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
    2.30 -    }
    2.31 +    val syntax = get_syntax
    2.32 +    val ok =
    2.33 +      if (syntax.isDefined) {
    2.34 +        val ok = parser(buffer, syntax.get, data)
    2.35 +        if (stopped) { root.add(new DefaultMutableTreeNode("<stopped>")); true }
    2.36 +        else ok
    2.37 +      }
    2.38 +      else false
    2.39 +    if (!ok) root.add(new DefaultMutableTreeNode("<ignored>"))
    2.40 +
    2.41      data
    2.42    }
    2.43  
    2.44 @@ -87,15 +92,14 @@
    2.45  
    2.46      val buffer = pane.getBuffer
    2.47      Isabelle.buffer_lock(buffer) {
    2.48 -      Document_Model(buffer) match {
    2.49 +      get_syntax match {
    2.50          case None => null
    2.51 -        case Some(model) =>
    2.52 +        case Some(syntax) =>
    2.53            val line = buffer.getLineOfOffset(caret)
    2.54            val start = buffer.getLineStartOffset(line)
    2.55            val text = buffer.getSegment(start, caret - start)
    2.56  
    2.57 -          val completion = model.session.recent_syntax().completion
    2.58 -          completion.complete(text) match {
    2.59 +          syntax.completion.complete(text) match {
    2.60              case None => null
    2.61              case Some((word, cs)) =>
    2.62                val ds =
    2.63 @@ -128,14 +132,13 @@
    2.64  }
    2.65  
    2.66  
    2.67 -class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
    2.68 +class Isabelle_Sidekick_Default
    2.69 +  extends Isabelle_Sidekick("isabelle", Isabelle.session.get_recent_syntax)
    2.70  {
    2.71    import Thy_Syntax.Structure
    2.72  
    2.73 -  def parser(data: SideKickParsedData, model: Document_Model)
    2.74 +  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
    2.75    {
    2.76 -    val syntax = model.session.recent_syntax()
    2.77 -
    2.78      def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
    2.79        entry match {
    2.80          case Structure.Block(name, body) =>
    2.81 @@ -157,36 +160,53 @@
    2.82          case _ => Nil
    2.83        }
    2.84  
    2.85 -    val text = Isabelle.buffer_text(model.buffer)
    2.86 -    val structure = Structure.parse(syntax, model.name, text)
    2.87 -
    2.88 -    make_tree(0, structure) foreach (node => data.root.add(node))
    2.89 +    Isabelle.buffer_node_name(buffer) match {
    2.90 +      case Some(node_name) =>
    2.91 +        val text = Isabelle.buffer_text(buffer)
    2.92 +        val structure = Structure.parse(syntax, node_name, text)
    2.93 +        make_tree(0, structure) foreach (node => data.root.add(node))
    2.94 +        true
    2.95 +      case None => false
    2.96 +    }
    2.97    }
    2.98  }
    2.99  
   2.100  
   2.101 -class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
   2.102 +class Isabelle_Sidekick_Options
   2.103 +  extends Isabelle_Sidekick("isabelle-options", Some(Options.options_syntax))
   2.104 +
   2.105 +
   2.106 +class Isabelle_Sidekick_Root
   2.107 +  extends Isabelle_Sidekick("isabelle-root", Some(Build.root_syntax))
   2.108 +
   2.109 +
   2.110 +class Isabelle_Sidekick_Raw
   2.111 +  extends Isabelle_Sidekick("isabelle-raw", Isabelle.session.get_recent_syntax)
   2.112  {
   2.113 -  def parser(data: SideKickParsedData, model: Document_Model)
   2.114 +  override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   2.115    {
   2.116 -    val root = data.root
   2.117 -    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
   2.118 -    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
   2.119 -      snapshot.state.command_state(snapshot.version, command).markup
   2.120 -        .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
   2.121 -          {
   2.122 -            val range = info.range + command_start
   2.123 -            val content = command.source(info.range).replace('\n', ' ')
   2.124 -            val info_text =
   2.125 -              Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
   2.126 +    Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
   2.127 +      case Some(snapshot) =>
   2.128 +        val root = data.root
   2.129 +        for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
   2.130 +          snapshot.state.command_state(snapshot.version, command).markup
   2.131 +            .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
   2.132 +              {
   2.133 +                val range = info.range + command_start
   2.134 +                val content = command.source(info.range).replace('\n', ' ')
   2.135 +                val info_text =
   2.136 +                  Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
   2.137  
   2.138 -            new DefaultMutableTreeNode(
   2.139 -              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
   2.140 -                override def getShortString: String = content
   2.141 -                override def getLongString: String = info_text
   2.142 -                override def toString = quote(content) + " " + range.toString
   2.143 +                new DefaultMutableTreeNode(
   2.144 +                  new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
   2.145 +                    override def getShortString: String = content
   2.146 +                    override def getLongString: String = info_text
   2.147 +                    override def toString = quote(content) + " " + range.toString
   2.148 +                  })
   2.149                })
   2.150 -          })
   2.151 +        }
   2.152 +        true
   2.153 +      case None => false
   2.154      }
   2.155    }
   2.156  }
     3.1 --- a/src/Tools/jEdit/src/jEdit.props	Tue Aug 07 20:28:35 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/jEdit.props	Tue Aug 07 21:38:24 2012 +0200
     3.3 @@ -180,14 +180,11 @@
     3.4  isabelle-output.dock-position=bottom
     3.5  isabelle-output.height=174
     3.6  isabelle-output.width=412
     3.7 +isabelle-readme.dock-position=bottom
     3.8  isabelle-session.dock-position=bottom
     3.9 -isabelle-readme.dock-position=bottom
    3.10  line-end.shortcut=END
    3.11  line-home.shortcut=HOME
    3.12  lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
    3.13 -mode.isabelle.customSettings=true
    3.14 -mode.isabelle.folding=sidekick
    3.15 -mode.isabelle.sidekick.showStatusWindow.label=true
    3.16  print.font=IsabelleText
    3.17  restore.remote=false
    3.18  restore=false
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 20:28:35 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 07 21:38:24 2012 +0200
     4.3 @@ -193,22 +193,24 @@
     4.4      }
     4.5    }
     4.6  
     4.7 +  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
     4.8 +  {
     4.9 +    val name = buffer_name(buffer)
    4.10 +    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
    4.11 +  }
    4.12 +
    4.13    def init_model(buffer: Buffer)
    4.14    {
    4.15      swing_buffer_lock(buffer) {
    4.16        val opt_model =
    4.17 -      {
    4.18 -        val name = buffer_name(buffer)
    4.19 -        Thy_Header.thy_name(name) match {
    4.20 -          case Some(theory) =>
    4.21 -            val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
    4.22 +        buffer_node_name(buffer) match {
    4.23 +          case Some(node_name) =>
    4.24              document_model(buffer) match {
    4.25                case Some(model) if model.name == node_name => Some(model)
    4.26                case _ => Some(Document_Model.init(session, buffer, node_name))
    4.27              }
    4.28            case None => None
    4.29          }
    4.30 -      }
    4.31        if (opt_model.isDefined) {
    4.32          for (text_area <- jedit_text_areas(buffer)) {
    4.33            if (document_view(text_area).map(_.model) != opt_model)
     5.1 --- a/src/Tools/jEdit/src/services.xml	Tue Aug 07 20:28:35 2012 +0200
     5.2 +++ b/src/Tools/jEdit/src/services.xml	Tue Aug 07 21:38:24 2012 +0200
     5.3 @@ -8,6 +8,12 @@
     5.4  	<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
     5.5  		new isabelle.jedit.Isabelle_Sidekick_Default();
     5.6  	</SERVICE>
     5.7 +	<SERVICE NAME="isabelle-options" CLASS="sidekick.SideKickParser">
     5.8 +		new isabelle.jedit.Isabelle_Sidekick_Options();
     5.9 +	</SERVICE>
    5.10 +	<SERVICE NAME="isabelle-root" CLASS="sidekick.SideKickParser">
    5.11 +		new isabelle.jedit.Isabelle_Sidekick_Root();
    5.12 +	</SERVICE>
    5.13  	<SERVICE NAME="isabelle-raw" CLASS="sidekick.SideKickParser">
    5.14  		new isabelle.jedit.Isabelle_Sidekick_Raw();
    5.15  	</SERVICE>