src/Pure/Isar/outer_syntax.ML
changeset 44357 5f5649ac8235
parent 44187 88d770052bac
child 44478 4fdb1009a370
equal deleted inserted replaced
44356:f6a2e5ce2ce5 44357:5f5649ac8235
    60 (* parse command *)
    60 (* parse command *)
    61 
    61 
    62 local
    62 local
    63 
    63 
    64 fun terminate false = Scan.succeed ()
    64 fun terminate false = Scan.succeed ()
    65   | terminate true = Parse.group "end of input" (Scan.option Parse.sync -- Parse.semicolon >> K ());
    65   | terminate true =
       
    66       Parse.group (fn () => "end of input")
       
    67         (Scan.option Parse.sync -- Parse.semicolon >> K ());
    66 
    68 
    67 fun body cmd (name, _) =
    69 fun body cmd (name, _) =
    68   (case cmd name of
    70   (case cmd name of
    69     SOME (Command {int_only, parse, ...}) =>
    71     SOME (Command {int_only, parse, ...}) =>
    70       Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))
    72       Parse.!!! (Scan.prompt (name ^ "# ") (Parse.tags |-- parse >> pair int_only))