more position information for markup;
authorwenzelm
Wed, 26 Jun 2013 09:58:39 +0200
changeset 52455 9a8f4fdac3cf
parent 52450 e09e1091394d
child 52456 960202346d0c
more position information for markup;
src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Tue Jun 25 20:38:06 2013 +0200
+++ b/src/Pure/pure_syn.ML	Wed Jun 26 09:58:39 2013 +0200
@@ -9,7 +9,8 @@
 
 val _ =
   Outer_Syntax.command
-    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context"
+    (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML")
+    "begin theory context"
     (Thy_Header.args >> (fn header =>
       Toplevel.print o
         Toplevel.init_theory
@@ -17,7 +18,8 @@
 
 val _ =
   Outer_Syntax.command
-    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file"
+    (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML")
+    "ML text from file"
     (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
         let
           val [{src_path, text, pos}] = files (Context.theory_of gthy);