misc tuning -- more uniform ML vs. Scala;

--- a/src/Pure/PIDE/resources.scala	Sat Mar 14 17:23:58 2015 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Mar 14 18:18:40 2015 +0100
@@ -86,20 +86,21 @@
     }
   }
 
-  def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
+  def check_thy_reader(qualifier: String, node_name: Document.Node.Name, reader: Reader[Char])
     : Document.Node.Header =
   {
     if (reader.source.length > 0) {
       try {
         val header = Thy_Header.read(reader).decode_symbols
 
-        val base_name = Long_Name.base_name(name.theory)
-        val name1 = header.name
-        if (base_name != name1)
+        val base_name = Long_Name.base_name(node_name.theory)
+        val (name, pos) = header.name
+        if (base_name != name)
           error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
-            " for theory " + quote(name1))
+            " for theory " + quote(name) + Position.here(pos))
 
-        val imports = header.imports.map(import_name(qualifier, name, _))
+        val imports =
+          header.imports.map({ case (s, _) => import_name(qualifier, node_name, s) })
         Document.Node.Header(imports, header.keywords, Nil)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }

--- a/src/Pure/Thy/thy_header.ML	Sat Mar 14 17:23:58 2015 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sat Mar 14 18:18:40 2015 +0100
@@ -103,8 +103,9 @@
 
 local
 
-val imports =
-  Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
+fun imports name =
+  if name = Context.PureN then Scan.succeed []
+  else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
 
 val opt_files =
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
@@ -128,7 +129,7 @@
 
 val args =
   Parse.position Parse.theory_name :|-- (fn (name, pos) =>
-    (if name = Context.PureN then Scan.succeed [] else imports) --
+    imports name --
     Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
     Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
 

--- a/src/Pure/Thy/thy_header.scala	Sat Mar 14 17:23:58 2015 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sat Mar 14 18:18:40 2015 +0100
@@ -80,11 +80,10 @@
 
   val header: Parser[Thy_Header] =
   {
-    val file_name = atom("file name", _.is_name)
-
     val opt_files =
       $$$("(") ~! (rep1sep(name, $$$(",")) <~ $$$(")")) ^^ { case _ ~ x => x } |
       success(Nil)
+
     val keyword_spec =
       atom("outer syntax keyword specification", _.is_name) ~ opt_files ~ tags ^^
       { case x ~ y ~ z => ((x, y), z) }
@@ -94,17 +93,14 @@
       opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
       opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
       { case xs ~ y ~ z => xs.map((_, y, z)) }
+
     val keyword_decls =
       keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
       { case xs ~ yss => (xs :: yss).flatten }
 
-    val file =
-      $$$("(") ~! (file_name ~ $$$(")")) ^^ { case _ ~ (x ~ _) => (x, false) } |
-      file_name ^^ (x => (x, true))
-
     val args =
-      theory_name ~
-      (opt($$$(IMPORTS) ~! (rep1(theory_xname))) ^^
+      position(theory_name) ~
+      (opt($$$(IMPORTS) ~! (rep1(position(theory_xname)))) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt($$$(KEYWORDS) ~! keyword_decls) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
@@ -156,19 +152,15 @@
 
 
 sealed case class Thy_Header(
-  name: String,
-  imports: List[String],
+  name: (String, Position.T),
+  imports: List[(String, Position.T)],
   keywords: Thy_Header.Keywords)
 {
-  def map(f: String => String): Thy_Header =
-    Thy_Header(f(name), imports.map(f), keywords)
-
   def decode_symbols: Thy_Header =
   {
     val f = Symbol.decode _
-    Thy_Header(f(name), imports.map(f),
+    Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
       keywords.map({ case (a, b, c) =>
         (f(a), b.map({ case ((x, y), z) => ((f(x), y.map(f)), z.map(f)) }), c.map(f)) }))
   }
 }
-