Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper file extension;
authorwenzelm
Tue, 05 Apr 2016 22:07:44 +0200
changeset 62881 20b0cb2f0b87
parent 62880 76e7d9169b54
child 62882 3c4161728aa8
proper file extension;
src/Pure/ML/ml_root.scala file | annotate | diff | comparison | revisions
src/Pure/ML_Root.thy file | annotate | diff | comparison | revisions 
--- a/src/Pure/ML/ml_root.scala	Tue Apr 05 21:51:14 2016 +0200
+++ b/src/Pure/ML/ml_root.scala	Tue Apr 05 22:07:44 2016 +0200
@@ -23,7 +23,7 @@
       (USE, Some((Keyword.THY_LOAD, Nil)), None) +
       (USE_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
       (USE_NO_DEBUG, Some((Keyword.THY_LOAD, Nil)), None) +
-      (USE_THY, Some((Keyword.THY_LOAD, Nil)), None)
+      (USE_THY, Some((Keyword.THY_LOAD, List("thy"))), None)
 
   private object Parser extends Parse.Parser
   {
--- a/src/Pure/ML_Root.thy	Tue Apr 05 21:51:14 2016 +0200
+++ b/src/Pure/ML_Root.thy	Tue Apr 05 22:07:44 2016 +0200
@@ -7,7 +7,7 @@
 theory ML_Root
 imports Pure
 keywords "use" "use_debug" "use_no_debug" :: thy_load
-  and "use_thy" :: thy_load
+  and "use_thy" :: thy_load ("thy")
 begin
 
 setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
isabelle