fall back on Isabelle system completion (symbols only);
authorwenzelm
Tue Jun 23 20:49:56 2009 +0200 (2009-06-23)
changeset 346125a03dc7a19e1
parent 34611 b40e43d70ae9
child 34613 71fb6ab6ec57
fall back on Isabelle system completion (symbols only);
tuned;
src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
src/Tools/jEdit/src/jedit/Plugin.scala
src/Tools/jEdit/src/prover/Prover.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Tue Jun 23 20:16:32 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Tue Jun 23 20:49:56 2009 +0200
     1.3 @@ -52,21 +52,19 @@
     1.4    override def complete(pane: EditPane, caret: Int): SideKickCompletion =
     1.5    {
     1.6      val buffer = pane.getBuffer
     1.7 -    Isabelle.prover_setup(buffer) match {
     1.8 -      case None => return null
     1.9 -      case Some(setup) =>
    1.10 -        val line = buffer.getLineOfOffset(caret)
    1.11 -        val start = buffer.getLineStartOffset(line)
    1.12 +
    1.13 +    val line = buffer.getLineOfOffset(caret)
    1.14 +    val start = buffer.getLineStartOffset(line)
    1.15 +    val text = buffer.getSegment(start, caret - start)
    1.16  
    1.17 -        if (caret == start) return null
    1.18 -        val text = buffer.getSegment(start, caret - start)
    1.19 +    val completion =
    1.20 +      Isabelle.prover_setup(buffer).map(_.prover.completion) getOrElse Isabelle.completion
    1.21  
    1.22 -        setup.prover.complete(text) match {
    1.23 -          case None => null
    1.24 -          case Some((word, cs)) =>
    1.25 -            new SideKickCompletion(pane.getView, word,
    1.26 -              cs.map(Isabelle.system.symbols.decode(_)).toArray.asInstanceOf[Array[Object]]) { }
    1.27 -        }
    1.28 +    completion.complete(text) match {
    1.29 +      case None => null
    1.30 +      case Some((word, cs)) =>
    1.31 +        new SideKickCompletion(pane.getView, word,
    1.32 +          cs.map(Isabelle.system.symbols.decode(_)).toArray.asInstanceOf[Array[Object]]) { }
    1.33      }
    1.34    }
    1.35  
     2.1 --- a/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Jun 23 20:16:32 2009 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Jun 23 20:49:56 2009 +0200
     2.3 @@ -38,6 +38,7 @@
     2.4    // Isabelle system instance
     2.5    var system: IsabelleSystem = null
     2.6    def symbols = system.symbols
     2.7 +  lazy val completion = new Completion + symbols
     2.8  
     2.9    // settings
    2.10    def default_logic = {
     3.1 --- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 23 20:16:32 2009 +0200
     3.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 23 20:49:56 2009 +0200
     3.3 @@ -78,9 +78,9 @@
     3.4  
     3.5    /* completions */
     3.6  
     3.7 -  private var completion = new Completion + isabelle_system.symbols
     3.8 -  decl_info += (p => completion += p._1)
     3.9 -  def complete(line: CharSequence): Option[(String, List[String])] = completion.complete(line)
    3.10 +  private var _completion = Isabelle.completion
    3.11 +  def completion = _completion
    3.12 +  decl_info += (p => _completion += p._1)
    3.13  
    3.14  
    3.15    /* event handling */