pass syntax through check_thy;

--- a/src/Pure/System/build.scala	Wed Aug 22 15:53:17 2012 +0200
+++ b/src/Pure/System/build.scala	Wed Aug 22 16:10:23 2012 +0200
@@ -354,7 +354,7 @@
                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
 
           val loaded_theories = thy_deps.loaded_theories
-          val syntax = thy_deps.syntax
+          val syntax = thy_deps.make_syntax
 
           val all_files =
             thy_deps.deps.map({ case (n, h) =>

--- a/src/Pure/Thy/thy_info.scala	Wed Aug 22 15:53:17 2012 +0200
+++ b/src/Pure/Thy/thy_info.scala	Wed Aug 22 16:10:23 2012 +0200
@@ -44,14 +44,10 @@
 
     def deps: List[Dep] = rev_deps.reverse
 
-    def thy_load_commands: List[String] =
-      (for ((cmd, Some(((Keyword.THY_LOAD, _), _))) <- keywords) yield cmd) :::
-        thy_load.base_syntax.thy_load_commands
-
     def loaded_theories: Set[String] =
       (thy_load.loaded_theories /: rev_deps) { case (loaded, (name, _)) => loaded + name.theory }
 
-    def syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
+    def make_syntax: Outer_Syntax = thy_load.base_syntax.add_keywords(keywords)
   }
 
   private def require_thys(initiators: List[Document.Node.Name],
@@ -66,8 +62,9 @@
     else {
       try {
         if (initiators.contains(name)) error(cycle_msg(initiators))
+        val syntax = required.make_syntax
         val header =
-          try { thy_load.check_thy(name) }
+          try { thy_load.check_thy(syntax, name) }
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred while examining theory " +

--- a/src/Pure/Thy/thy_load.scala	Wed Aug 22 15:53:17 2012 +0200
+++ b/src/Pure/Thy/thy_load.scala	Wed Aug 22 16:10:23 2012 +0200
@@ -42,12 +42,14 @@
     }
   }
 
-  def check_thy_text(name: Document.Node.Name, text: CharSequence): Document.Node.Header =
+  def check_thy_text(syntax: Outer_Syntax, name: Document.Node.Name, text: CharSequence)
+    : Document.Node.Header =
   {
     val header = Thy_Header.read(text)
     val name1 = header.name
     val imports = header.imports.map(import_name(name.dir, _))
     // FIXME val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
+    // FIXME find files in text
     val uses = header.uses
     if (name.theory != name1)
       error("Bad file name " + Thy_Load.thy_path(Path.basic(name.theory)) +
@@ -55,11 +57,11 @@
     Document.Node.Header(imports, header.keywords, uses)
   }
 
-  def check_thy(name: Document.Node.Name): Document.Node.Header =
+  def check_thy(syntax: Outer_Syntax, name: Document.Node.Name): Document.Node.Header =
   {
     val path = Path.explode(name.node)
     if (!path.is_file) error("No such file: " + path.toString)
-    check_thy_text(name, File.read(path))
+    check_thy_text(syntax, name, File.read(path))
   }
 }
 

--- a/src/Tools/jEdit/src/document_model.scala	Wed Aug 22 15:53:17 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Aug 22 16:10:23 2012 +0200
@@ -68,7 +68,8 @@
     Swing_Thread.require()
     Isabelle.buffer_lock(buffer) {
       Exn.capture {
-        Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
+        val text = buffer.getSegment(0, buffer.getLength)
+        Isabelle.thy_load.check_thy_text(session.recent_syntax, name, text)
       } match {
         case Exn.Res(header) => header
         case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))

--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 15:53:17 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Aug 22 16:10:23 2012 +0200
@@ -53,20 +53,21 @@
     }
   }
 
-  override def check_thy(name: Document.Node.Name): Document.Node.Header =
+  override def check_thy(syntax: Outer_Syntax, name: Document.Node.Name)
+    : Document.Node.Header =
   {
     Swing_Thread.now {
       Isabelle.jedit_buffer(name.node) match {
         case Some(buffer) =>
           Isabelle.buffer_lock(buffer) {
-            Some(check_thy_text(name, buffer.getSegment(0, buffer.getLength)))
+            Some(check_thy_text(syntax, name, buffer.getSegment(0, buffer.getLength)))
           }
         case None => None
       }
     } getOrElse {
       val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
       if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
-      check_thy_text(name, File.read(file))
+      check_thy_text(syntax, name, File.read(file))
     }
   }
 }