clarified files;
authorwenzelm
Tue Apr 05 21:51:14 2016 +0200 (2016-04-05)
changeset 6288076e7d9169b54
parent 62879 4764473c9b8d
child 62881 20b0cb2f0b87
clarified files;
src/Pure/ML/ML_Root.thy
src/Pure/ML_Root.thy
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/ML/ML_Root.thy	Tue Apr 05 21:23:32 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,41 +0,0 @@
     1.4 -(*  Title:      Pure/ML/ML_Root.thy
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Support for ML project ROOT file, with imitation of ML "use" commands.
     1.8 -*)
     1.9 -
    1.10 -theory ML_Root
    1.11 -imports "../Pure"
    1.12 -keywords "use" "use_debug" "use_no_debug" :: thy_load
    1.13 -  and "use_thy" :: thy_load
    1.14 -begin
    1.15 -
    1.16 -setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
    1.17 -
    1.18 -ML \<open>
    1.19 -local
    1.20 -
    1.21 -val _ =
    1.22 -  Outer_Syntax.command @{command_keyword use}
    1.23 -    "read and evaluate Isabelle/ML or SML file"
    1.24 -    (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE);
    1.25 -
    1.26 -val _ =
    1.27 -  Outer_Syntax.command @{command_keyword use_debug}
    1.28 -    "read and evaluate Isabelle/ML or SML file (with debugger information)"
    1.29 -    (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true));
    1.30 -
    1.31 -val _ =
    1.32 -  Outer_Syntax.command @{command_keyword use_no_debug}
    1.33 -    "read and evaluate Isabelle/ML or SML file (no debugger information)"
    1.34 -    (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
    1.35 -
    1.36 -val _ =
    1.37 -  Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
    1.38 -    (Parse.path -- @{keyword ";"} >> (fn _ =>
    1.39 -      Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
    1.40 -
    1.41 -in end
    1.42 -\<close>
    1.43 -
    1.44 -end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML_Root.thy	Tue Apr 05 21:51:14 2016 +0200
     2.3 @@ -0,0 +1,41 @@
     2.4 +(*  Title:      Pure/ML_Root.thy
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Support for ML project ROOT file, with imitation of ML "use" commands.
     2.8 +*)
     2.9 +
    2.10 +theory ML_Root
    2.11 +imports Pure
    2.12 +keywords "use" "use_debug" "use_no_debug" :: thy_load
    2.13 +  and "use_thy" :: thy_load
    2.14 +begin
    2.15 +
    2.16 +setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
    2.17 +
    2.18 +ML \<open>
    2.19 +local
    2.20 +
    2.21 +val _ =
    2.22 +  Outer_Syntax.command @{command_keyword use}
    2.23 +    "read and evaluate Isabelle/ML or SML file"
    2.24 +    (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE);
    2.25 +
    2.26 +val _ =
    2.27 +  Outer_Syntax.command @{command_keyword use_debug}
    2.28 +    "read and evaluate Isabelle/ML or SML file (with debugger information)"
    2.29 +    (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true));
    2.30 +
    2.31 +val _ =
    2.32 +  Outer_Syntax.command @{command_keyword use_no_debug}
    2.33 +    "read and evaluate Isabelle/ML or SML file (no debugger information)"
    2.34 +    (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
    2.35 +
    2.36 +val _ =
    2.37 +  Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
    2.38 +    (Parse.path -- @{keyword ";"} >> (fn _ =>
    2.39 +      Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
    2.40 +
    2.41 +in end
    2.42 +\<close>
    2.43 +
    2.44 +end
     3.1 --- a/src/Pure/ROOT	Tue Apr 05 21:23:32 2016 +0200
     3.2 +++ b/src/Pure/ROOT	Tue Apr 05 21:51:14 2016 +0200
     3.3 @@ -4,6 +4,6 @@
     3.4    global_theories
     3.5      Pure
     3.6    theories
     3.7 -    "ML/ML_Root"
     3.8 +    ML_Root
     3.9    files
    3.10      "ROOT.ML"
     4.1 --- a/src/Pure/ROOT.ML	Tue Apr 05 21:23:32 2016 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Tue Apr 05 21:51:14 2016 +0200
     4.3 @@ -339,4 +339,4 @@
     4.4  use_thy "Pure";
     4.5  
     4.6  use "ML/ml_pervasive_final.ML";
     4.7 -use_thy "ML/ML_Root";
     4.8 +use_thy "ML_Root";