provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
authorwenzelm
Sun Jan 10 15:15:04 2010 +0100 (2010-01-10)
changeset 34851304a86164dd2
parent 34850 fdd560e80264
child 34852 d21c997104c4
provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
src/Tools/jEdit/src/jedit/scala_console.scala
src/Tools/jEdit/src/proofdocument/session.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/scala_console.scala	Sat Jan 09 23:28:52 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/scala_console.scala	Sun Jan 10 15:15:04 2010 +0100
     1.3 @@ -106,7 +106,7 @@
     1.4      }
     1.5      interp.setContextClassLoader
     1.6      interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
     1.7 -    interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session)
     1.8 +    interp.interpret("import isabelle.jedit.Isabelle")
     1.9  
    1.10      interpreters += (console -> interp)
    1.11    }
    1.12 @@ -121,8 +121,8 @@
    1.13      out.print(null,
    1.14       "This shell evaluates Isabelle/Scala expressions.\n\n" +
    1.15       "The following special toplevel bindings are provided:\n" +
    1.16 -     "  view    -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
    1.17 -     "  session -- Isabelle session (e.g. session.isabelle_system)\n")
    1.18 +     "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
    1.19 +     "  Isabelle  -- main Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
    1.20    }
    1.21  
    1.22    override def printPrompt(console: Console, out: Output)
     2.1 --- a/src/Tools/jEdit/src/proofdocument/session.scala	Sat Jan 09 23:28:52 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/session.scala	Sun Jan 10 15:15:04 2010 +0100
     2.3 @@ -30,7 +30,7 @@
     2.4  }
     2.5  
     2.6  
     2.7 -class Session(val isabelle_system: Isabelle_System)
     2.8 +class Session(system: Isabelle_System)
     2.9  {
    2.10    /* pervasive event buses */
    2.11  
    2.12 @@ -50,7 +50,7 @@
    2.13  
    2.14    /** main actor **/
    2.15  
    2.16 -  @volatile private var syntax = new Outer_Syntax(isabelle_system.symbols)
    2.17 +  @volatile private var syntax = new Outer_Syntax(system.symbols)
    2.18    def current_syntax: Outer_Syntax = syntax
    2.19  
    2.20    @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
    2.21 @@ -90,7 +90,7 @@
    2.22                case Some(command) =>
    2.23                  if (!lookup_command(command.id).isDefined) {
    2.24                    register(command)
    2.25 -                  prover.define_command(command.id, isabelle_system.symbols.encode(command.content))
    2.26 +                  prover.define_command(command.id, system.symbols.encode(command.content))
    2.27                  }
    2.28                  Some(command.id)
    2.29              })
    2.30 @@ -203,7 +203,7 @@
    2.31        react {
    2.32          case Start(timeout, args) =>
    2.33            if (prover == null) {
    2.34 -            prover = new Isabelle_Process(isabelle_system, self, args:_*) with Isar_Document
    2.35 +            prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
    2.36              val origin = sender
    2.37              val opt_err = prover_startup(timeout)
    2.38              if (opt_err.isDefined) prover = null