# HG changeset patch
# User wenzelm
# Date 1263070955 -3600
# Node ID 77ac1383397265861f2bd7567180636464804ebd
# Parent  1c31074598e38031cf394fc0e516fad56e2a8e03
export isabelle_system, e.g. for use via "session" in Isabelle/Scala interpreter;

diff -r 1c31074598e3 -r 77ac13833972 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Sat Jan 09 21:31:59 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Sat Jan 09 22:02:35 2010 +0100
@@ -30,7 +30,7 @@
 }
 
 
-class Session(system: Isabelle_System)
+class Session(val isabelle_system: Isabelle_System)
 {
   /* pervasive event buses */
 
@@ -50,7 +50,7 @@
 
   /** main actor **/
 
-  @volatile private var syntax = new Outer_Syntax(system.symbols)
+  @volatile private var syntax = new Outer_Syntax(isabelle_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, system.symbols.encode(command.content))
+                  prover.define_command(command.id, isabelle_system.symbols.encode(command.content))
                 }
                 Some(command.id)
             })
@@ -203,7 +203,7 @@
       react {
         case Start(timeout, args) =>
           if (prover == null) {
-            prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
+            prover = new Isabelle_Process(isabelle_system, self, args:_*) with Isar_Document
             val origin = sender
             val opt_err = prover_startup(timeout)
             if (opt_err.isDefined) prover = null