src/Pure/ML/ML_Root.thy
changeset 62871 4a6cbe1239fe
parent 62868 61a691db1c4d
child 62873 2f9c8a18f832
equal deleted inserted replaced
62870:cf724647f75b 62871:4a6cbe1239fe
    14 local
    14 local
    15 
    15 
    16 val _ =
    16 val _ =
    17   Outer_Syntax.command @{command_keyword use}
    17   Outer_Syntax.command @{command_keyword use}
    18     "read and evaluate Isabelle/ML or SML file"
    18     "read and evaluate Isabelle/ML or SML file"
    19     (Resources.parse_files "use" >> ML_File.use NONE);
    19     (Resources.parse_files "use" --| @{keyword ";"} >> ML_File.use NONE);
    20 
    20 
    21 val _ =
    21 val _ =
    22   Outer_Syntax.command @{command_keyword use_debug}
    22   Outer_Syntax.command @{command_keyword use_debug}
    23     "read and evaluate Isabelle/ML or SML file (with debugger information)"
    23     "read and evaluate Isabelle/ML or SML file (with debugger information)"
    24     (Resources.parse_files "use_debug" >> ML_File.use (SOME true));
    24     (Resources.parse_files "use_debug" --| @{keyword ";"} >> ML_File.use (SOME true));
    25 
    25 
    26 val _ =
    26 val _ =
    27   Outer_Syntax.command @{command_keyword use_no_debug}
    27   Outer_Syntax.command @{command_keyword use_no_debug}
    28     "read and evaluate Isabelle/ML or SML file (no debugger information)"
    28     "read and evaluate Isabelle/ML or SML file (no debugger information)"
    29     (Resources.parse_files "use_no_debug" >> ML_File.use (SOME false));
    29     (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> ML_File.use (SOME false));
    30 
    30 
    31 val _ =
    31 val _ =
    32   Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
    32   Outer_Syntax.command @{command_keyword use_thy} "undefined dummy command"
    33     (Scan.succeed (Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
    33     (Parse.path -- @{keyword ";"} >> (fn _ =>
       
    34       Toplevel.keep (fn _ => error "Undefined command 'use_thy'")));
    34 
    35 
    35 in end
    36 in end
    36 \<close>
    37 \<close>
    37 
    38 
    38 end
    39 end