src/Pure/Isar/isar_syn.ML
changeset 25585 19cd3474fdf3
parent 25578 11ee8b183477
child 25588 514ae4e4d164
equal deleted inserted replaced
25584:222b91dd754c 25585:19cd3474fdf3
   751 val _ =
   751 val _ =
   752   OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
   752   OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
   753     (P.position P.string :|-- (fn (str, pos) =>
   753     (P.position P.string :|-- (fn (str, pos) =>
   754       (case OuterSyntax.parse pos str of
   754       (case OuterSyntax.parse pos str of
   755         [transition] => Scan.succeed (K transition)
   755         [transition] => Scan.succeed (K transition)
   756       | _ => Scan.fail_with (K "exactly one nested Isabelle command expected"))
   756       | _ => Scan.fail_with (K "exactly one nested command expected"))
   757       handle ERROR msg => Scan.fail_with (K ("malformed nested command\n" ^ msg))));
   757       handle ERROR msg => Scan.fail_with (K ("malformed command\n" ^ msg))));
   758 
   758 
   759 
   759 
   760 
   760 
   761 (** diagnostic commands (for interactive mode only) **)
   761 (** diagnostic commands (for interactive mode only) **)
   762 
   762