tunes signature -- more uniform ML vs. Scala;
--- 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 --| $$$ ")") "";
--- 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] =
--- 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));