# HG changeset patch
# User wenzelm
# Date 1459864738 -7200
# Node ID 61a691db1c4d99a643229c77a8e2c6fa29d2b72d
# Parent  cce0570d1bfa23382e0d574eefe2249edecb2de1
support for ML project ROOT file, with imitation of ML "use" commands;

diff -r cce0570d1bfa -r 61a691db1c4d src/Pure/ML/ML_Root.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ML_Root.thy	Tue Apr 05 15:58:58 2016 +0200
@@ -0,0 +1,38 @@
+(*  Title:      Pure/ML/ML_Root.thy
+    Author:     Makarius
+
+Support for ML project ROOT file, with imitation of ML "use" commands.
+*)
+
+theory ML_Root
+imports "../Pure"
+keywords "use" "use_debug" "use_no_debug" :: thy_load
+  and "use_thy" :: thy_load
+begin
+
+ML \<open>
+local
+
+val _ =
+  Outer_Syntax.command @{command_keyword use}
+    "read and evaluate Isabelle/ML or SML file"
+    (Resources.parse_files "use" >> ML_File.use NONE);
+
+val _ =
+  Outer_Syntax.command @{command_keyword use_debug}
+    "read and evaluate Isabelle/ML or SML file (with debugger information)"
+    (Resources.parse_files "use_debug" >> ML_File.use (SOME true));
+
+val _ =
+  Outer_Syntax.command @{command_keyword use_no_debug}
+    "read and evaluate Isabelle/ML or SML file (no debugger information)"
+    (Resources.parse_files "use_no_debug" >> ML_File.use (SOME false));
+
+val _ =
+  Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
+    (Scan.succeed (Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
+
+in end
+\<close>
+
+end
diff -r cce0570d1bfa -r 61a691db1c4d src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Tue Apr 05 15:53:48 2016 +0200
+++ b/src/Pure/ML/ml_file.ML	Tue Apr 05 15:58:58 2016 +0200
@@ -8,7 +8,7 @@
 sig
   val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
   val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
-  val any: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
+  val use: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure ML_File: ML_FILE =
@@ -32,7 +32,7 @@
 val ML = command (K false);
 val SML = command (K true);
 
-val any =
+val use =
   command (fn path =>
     (case try (#2 o Path.split_ext) path of
       SOME "ML" => false
diff -r cce0570d1bfa -r 61a691db1c4d src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Apr 05 15:53:48 2016 +0200
+++ b/src/Pure/ROOT	Tue Apr 05 15:58:58 2016 +0200
@@ -1,5 +1,9 @@
 chapter Pure
 
 session Pure =
-  global_theories Pure
-  files "ROOT.ML"
+  global_theories
+    Pure
+  theories
+    "ML/ML_Root"
+  files
+    "ROOT.ML"