src/Pure/Isar/toplevel.ML
changeset 6971 4a13e098ee86
parent 6965 a766de752996
child 7022 abf9d5e2fb6e
equal deleted inserted replaced
6970:ac37a8fcaad1 6971:4a13e098ee86
   331 
   331 
   332 fun exn_message TERMINATE = "Exit."
   332 fun exn_message TERMINATE = "Exit."
   333   | exn_message RESTART = "Restart."
   333   | exn_message RESTART = "Restart."
   334   | exn_message (BREAK _) = "Break."
   334   | exn_message (BREAK _) = "Break."
   335   | exn_message (FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
   335   | exn_message (FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
   336   | exn_message Interrupt = "Interrupt (exec)."
   336   | exn_message Interrupt = "Interrupt."
   337   | exn_message ERROR = "ERROR."
   337   | exn_message ERROR = "ERROR."
   338   | exn_message (ERROR_MESSAGE msg) = msg
   338   | exn_message (ERROR_MESSAGE msg) = msg
   339   | exn_message (THEORY (msg, _)) = msg
   339   | exn_message (THEORY (msg, _)) = msg
   340   | exn_message (ProofContext.CONTEXT (msg, _)) = msg
   340   | exn_message (ProofContext.CONTEXT (msg, _)) = msg
   341   | exn_message (Proof.STATE (msg, _)) = msg
   341   | exn_message (Proof.STATE (msg, _)) = msg
   450         check_stale state'; print_exn exn_info;
   450         check_stale state'; print_exn exn_info;
   451         true));
   451         true));
   452 
   452 
   453 fun raw_loop src =
   453 fun raw_loop src =
   454   (case get_interruptible (Source.set_prompt (prompt_state (get_state ())) src) of
   454   (case get_interruptible (Source.set_prompt (prompt_state (get_state ())) src) of
   455     None => (writeln "\nInterrupt (read)."; raw_loop src)
   455     None => (writeln "\nInterrupt."; raw_loop src)
   456   | Some None => ()
   456   | Some None => ()
   457   | Some (Some (tr, src')) => if >> tr then raw_loop src' else ());
   457   | Some (Some (tr, src')) => if >> tr then raw_loop src' else ());
   458 
   458 
   459 
   459 
   460 fun loop src = mask_interrupt raw_loop src;
   460 fun loop src = mask_interrupt raw_loop src;