src/Pure/System/session.scala
changeset 43673 29eb1cd29961
parent 43662 e3175ec00311
child 43695 5130dfe1b7be
equal deleted inserted replaced
43672:e9f26e66692d 43673:29eb1cd29961
   113 
   113 
   114   /** main protocol actor **/
   114   /** main protocol actor **/
   115 
   115 
   116   /* global state */
   116   /* global state */
   117 
   117 
       
   118   @volatile var loaded_theories: Set[String] = Set()
       
   119 
   118   @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
   120   @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
   119   def current_syntax(): Outer_Syntax = syntax
   121   def current_syntax(): Outer_Syntax = syntax
   120 
   122 
   121   @volatile private var reverse_syslog = List[XML.Elem]()
   123   @volatile private var reverse_syslog = List[XML.Elem]()
   122   def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
   124   def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
   136 
   138 
   137   /* theory files */
   139   /* theory files */
   138 
   140 
   139   val thy_load = new Thy_Load
   141   val thy_load = new Thy_Load
   140   {
   142   {
       
   143     override def is_loaded(name: String): Boolean =
       
   144       loaded_theories.contains(name)
       
   145 
   141     override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
   146     override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
   142     {
   147     {
   143       val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
   148       val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
   144       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
   149       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
   145       val text = Standard_System.read_file(file)
   150       val text = Standard_System.read_file(file)
   253                   assignments.event(Session.Assignment)
   258                   assignments.event(Session.Assignment)
   254                 }
   259                 }
   255                 catch { case _: Document.State.Fail => bad_result(result) }
   260                 catch { case _: Document.State.Fail => bad_result(result) }
   256               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   261               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
   257               case List(Keyword.Keyword_Decl(name)) => syntax += name
   262               case List(Keyword.Keyword_Decl(name)) => syntax += name
       
   263               case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
   258               case _ => bad_result(result)
   264               case _ => bad_result(result)
   259             }
   265             }
   260           }
   266           }
   261           else bad_result(result)
   267           else bad_result(result)
   262         }
   268         }