# HG changeset patch
# User wenzelm
# Date 1426350238 -3600
# Node ID d96cb03caf9e9a9623989ff2c8127bb61325e21a
# Parent  03aa1b63af10229634f2eec6c339cc80e344911b
tunes signature -- more uniform ML vs. Scala;

diff -r 03aa1b63af10 -r d96cb03caf9e src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sat Mar 14 16:56:11 2015 +0100
+++ b/src/Pure/Isar/parse.ML	Sat Mar 14 17:23:58 2015 +0100
@@ -69,6 +69,8 @@
   val xname: xstring parser
   val text: string parser
   val path: string parser
+  val theory_name: bstring parser
+  val theory_xname: xstring parser
   val liberal_name: xstring parser
   val parname: string parser
   val parbinding: binding parser
@@ -275,6 +277,9 @@
 
 val path = group (fn () => "file name/path specification") name;
 
+val theory_name = group (fn () => "theory name") name;
+val theory_xname = group (fn () => "theory name reference") xname;
+
 val liberal_name = keyword_with Token.ident_or_symbolic || xname;
 
 val parname = Scan.optional ($$$ "(" |-- name --| $$$ ")") "";
diff -r 03aa1b63af10 -r d96cb03caf9e src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Sat Mar 14 16:56:11 2015 +0100
+++ b/src/Pure/Isar/parse.scala	Sat Mar 14 17:23:58 2015 +0100
@@ -72,8 +72,10 @@
     def text: Parser[String] = atom("text", _.is_text)
     def ML_source: Parser[String] = atom("ML source", _.is_text)
     def document_source: Parser[String] = atom("document source", _.is_text)
+
     def path: Parser[String] =
       atom("file name/path specification", tok => tok.is_name && Path.is_wellformed(tok.content))
+
     def theory_name: Parser[String] =
       atom("theory name", tok => tok.is_name && Path.is_wellformed(tok.content))
     def theory_xname: Parser[String] =
diff -r 03aa1b63af10 -r d96cb03caf9e src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sat Mar 14 16:56:11 2015 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sat Mar 14 17:23:58 2015 +0100
@@ -103,10 +103,8 @@
 
 local
 
-val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
-val theory_xname = Parse.group (fn () => "theory name reference") (Parse.position Parse.xname);
-
-val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_xname);
+val imports =
+  Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_xname));
 
 val opt_files =
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
@@ -129,7 +127,7 @@
 in
 
 val args =
-  theory_name :|-- (fn (name, pos) =>
+  Parse.position Parse.theory_name :|-- (fn (name, pos) =>
     (if name = Context.PureN then Scan.succeed [] else imports) --
     Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
     Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));