# HG changeset patch
# User wenzelm
# Date 1380308697 -7200
# Node ID 65bca53daf70e67f5d8d27c199e0bab80e1542be
# Parent  16d9ecdf519a06698dd5f480e3bcc08ea609aee4
more robust parser: 'imports' are mandatory except for bootstrapping Pure;

diff -r 16d9ecdf519a -r 65bca53daf70 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Fri Sep 27 20:13:35 2013 +0200
+++ b/src/Pure/Thy/thy_header.ML	Fri Sep 27 21:04:57 2013 +0200
@@ -84,6 +84,8 @@
 
 val theory_name = Parse.group (fn () => "theory name") (Parse.position Parse.name);
 
+val imports = Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name);
+
 val opt_files =
   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
 
@@ -105,11 +107,10 @@
 in
 
 val args =
-  theory_name --
-  Scan.optional (Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 theory_name)) [] --
-  Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
-  Parse.$$$ beginN >>
-  (fn ((name, imports), keywords) => make name imports keywords);
+  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));
 
 end;