# HG changeset patch # User wenzelm # Date 1459872971 -7200 # Node ID 4a6cbe1239fe7d4f0d1178d6726e45a66aad1d7b # Parent cf724647f75b9af8c1a284720ca4ae807a8cb9c1 proper syntax; diff -r cf724647f75b -r 4a6cbe1239fe src/Pure/ML/ML_Root.thy --- a/src/Pure/ML/ML_Root.thy Tue Apr 05 17:25:11 2016 +0200 +++ b/src/Pure/ML/ML_Root.thy Tue Apr 05 18:16:11 2016 +0200 @@ -16,21 +16,22 @@ val _ = Outer_Syntax.command @{command_keyword use} "read and evaluate Isabelle/ML or SML file" - (Resources.parse_files "use" >> ML_File.use NONE); + (Resources.parse_files "use" --| @{keyword ";"} >> 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)); + (Resources.parse_files "use_debug" --| @{keyword ";"} >> 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)); + (Resources.parse_files "use_no_debug" --| @{keyword ";"} >> 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'"))); + (Parse.path -- @{keyword ";"} >> (fn _ => + Toplevel.keep (fn _ => error "Undefined command 'use_thy'"))); in end \