src/Pure/Isar/runtime.ML
changeset 49647 21ae8500d261
parent 48992 0518bf89c777
child 50201 c26369c9eda6
equal deleted inserted replaced
49646:77a0a53caa2f 49647:21ae8500d261
    74               TERMINATE => "Exit"
    74               TERMINATE => "Exit"
    75             | TimeLimit.TimeOut => "Timeout"
    75             | TimeLimit.TimeOut => "Timeout"
    76             | TOPLEVEL_ERROR => "Error"
    76             | TOPLEVEL_ERROR => "Error"
    77             | ERROR msg => msg
    77             | ERROR msg => msg
    78             | Fail msg => raised exn "Fail" [msg]
    78             | Fail msg => raised exn "Fail" [msg]
       
    79             | Output.TRACING_LIMIT n => "Tracing limit exceeded: " ^ string_of_int n
    79             | THEORY (msg, thys) =>
    80             | THEORY (msg, thys) =>
    80                 raised exn "THEORY" (msg :: map Context.str_of_thy thys)
    81                 raised exn "THEORY" (msg :: map Context.str_of_thy thys)
    81             | Ast.AST (msg, asts) =>
    82             | Ast.AST (msg, asts) =>
    82                 raised exn "AST" (msg :: map (Pretty.string_of o Ast.pretty_ast) asts)
    83                 raised exn "AST" (msg :: map (Pretty.string_of o Ast.pretty_ast) asts)
    83             | TYPE (msg, Ts, ts) =>
    84             | TYPE (msg, Ts, ts) =>