# HG changeset patch
# User wenzelm
# Date 1263132904 -3600
# Node ID 304a86164dd248122e8a7c6acf089d36737f674c
# Parent  fdd560e80264839bf353bdf0636b1135c9d20506
provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;

diff -r fdd560e80264 -r 304a86164dd2 src/Tools/jEdit/src/jedit/scala_console.scala
--- a/src/Tools/jEdit/src/jedit/scala_console.scala	Sat Jan 09 23:28:52 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/scala_console.scala	Sun Jan 10 15:15:04 2010 +0100
@@ -106,7 +106,7 @@
     }
     interp.setContextClassLoader
     interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
-    interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session)
+    interp.interpret("import isabelle.jedit.Isabelle")
 
     interpreters += (console -> interp)
   }
@@ -121,8 +121,8 @@
     out.print(null,
      "This shell evaluates Isabelle/Scala expressions.\n\n" +
      "The following special toplevel bindings are provided:\n" +
-     "  view    -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
-     "  session -- Isabelle session (e.g. session.isabelle_system)\n")
+     "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
+     "  Isabelle  -- main Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
   }
 
   override def printPrompt(console: Console, out: Output)
diff -r fdd560e80264 -r 304a86164dd2 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Sat Jan 09 23:28:52 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Sun Jan 10 15:15:04 2010 +0100
@@ -30,7 +30,7 @@
 }
 
 
-class Session(val isabelle_system: Isabelle_System)
+class Session(system: Isabelle_System)
 {
   /* pervasive event buses */
 
@@ -50,7 +50,7 @@
 
   /** main actor **/
 
-  @volatile private var syntax = new Outer_Syntax(isabelle_system.symbols)
+  @volatile private var syntax = new Outer_Syntax(system.symbols)
   def current_syntax: Outer_Syntax = syntax
 
   @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
@@ -90,7 +90,7 @@
               case Some(command) =>
                 if (!lookup_command(command.id).isDefined) {
                   register(command)
-                  prover.define_command(command.id, isabelle_system.symbols.encode(command.content))
+                  prover.define_command(command.id, system.symbols.encode(command.content))
                 }
                 Some(command.id)
             })
@@ -203,7 +203,7 @@
       react {
         case Start(timeout, args) =>
           if (prover == null) {
-            prover = new Isabelle_Process(isabelle_system, self, args:_*) with Isar_Document
+            prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
             val origin = sender
             val opt_err = prover_startup(timeout)
             if (opt_err.isDefined) prover = null