clarified build errors;
authorwenzelm
Sat May 27 13:20:35 2017 +0200 (2017-05-27 ago)
changeset 65948de7888573ed7
parent 65947 223fd19ac6b3
child 65949 453cf5c94345
clarified build errors;
tuned signature;
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Isar/runtime.ML	Sat May 27 13:07:27 2017 +0200
     1.2 +++ b/src/Pure/Isar/runtime.ML	Sat May 27 13:20:35 2017 +0200
     1.3 @@ -13,8 +13,8 @@
     1.4    val exn_context: Proof.context option -> exn -> exn
     1.5    val thread_context: exn -> exn
     1.6    type error = ((serial * string) * string option)
     1.7 -  val exn_messages_ids: exn -> error list
     1.8 -  val exn_messages: exn -> (serial * string) list
     1.9 +  val exn_messages: exn -> error list
    1.10 +  val exn_message_list: exn -> string list
    1.11    val exn_message: exn -> string
    1.12    val exn_error_message: exn -> unit
    1.13    val exn_system_message: exn -> unit
    1.14 @@ -91,7 +91,7 @@
    1.15  
    1.16  in
    1.17  
    1.18 -fun exn_messages_ids e =
    1.19 +fun exn_messages e =
    1.20    let
    1.21      fun raised exn name msgs =
    1.22        let val pos = Position.here (Exn_Properties.position exn) in
    1.23 @@ -141,12 +141,12 @@
    1.24  
    1.25  end;
    1.26  
    1.27 -fun exn_messages exn = map #1 (exn_messages_ids exn);
    1.28 +fun exn_message_list exn =
    1.29 +  (case exn_messages exn of
    1.30 +    [] => ["Interrupt"]
    1.31 +  | msgs => map (#2 o #1) msgs);
    1.32  
    1.33 -fun exn_message exn =
    1.34 -  (case exn_messages exn of
    1.35 -    [] => "Interrupt"
    1.36 -  | msgs => cat_lines (map snd msgs));
    1.37 +val exn_message = cat_lines o exn_message_list;
    1.38  
    1.39  val exn_error_message = Output.error_message o exn_message;
    1.40  val exn_system_message = Output.system_message o exn_message;
     2.1 --- a/src/Pure/Isar/toplevel.ML	Sat May 27 13:07:27 2017 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Sat May 27 13:20:35 2017 +0200
     2.3 @@ -593,7 +593,7 @@
     2.4  fun command_errors int tr st =
     2.5    (case transition int tr st of
     2.6      (st', NONE) => ([], SOME st')
     2.7 -  | (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE));
     2.8 +  | (_, SOME (exn, _)) => (Runtime.exn_messages exn, NONE));
     2.9  
    2.10  fun command_exception int tr st =
    2.11    (case transition int tr st of
     3.1 --- a/src/Pure/PIDE/command.ML	Sat May 27 13:07:27 2017 +0200
     3.2 +++ b/src/Pure/PIDE/command.ML	Sat May 27 13:20:35 2017 +0200
     3.3 @@ -201,7 +201,7 @@
     3.4          (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
     3.5            handle exn =>
     3.6              if Exn.is_interrupt exn then Exn.reraise exn
     3.7 -            else Runtime.exn_messages_ids exn)) ();
     3.8 +            else Runtime.exn_messages exn)) ();
     3.9  
    3.10  fun report tr m =
    3.11    Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
    3.12 @@ -293,7 +293,7 @@
    3.13    (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
    3.14      handle exn =>
    3.15        if Exn.is_interrupt exn then Exn.reraise exn
    3.16 -      else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
    3.17 +      else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn);
    3.18  
    3.19  fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
    3.20  
     4.1 --- a/src/Pure/PIDE/execution.ML	Sat May 27 13:07:27 2017 +0200
     4.2 +++ b/src/Pure/PIDE/execution.ML	Sat May 27 13:20:35 2017 +0200
     4.3 @@ -118,7 +118,7 @@
     4.4                      status task [Markup.finished];
     4.5                      Output.report [Markup.markup_only (Markup.bad ())];
     4.6                      if exec_id = 0 then ()
     4.7 -                    else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
     4.8 +                    else List.app (Future.error_message pos) (Runtime.exn_messages exn))
     4.9                  | Exn.Res _ =>
    4.10                      status task [Markup.finished])
    4.11              in Exn.release result end);
     5.1 --- a/src/Pure/Tools/build.ML	Sat May 27 13:07:27 2017 +0200
     5.2 +++ b/src/Pure/Tools/build.ML	Sat May 27 13:20:35 2017 +0200
     5.3 @@ -225,7 +225,7 @@
     5.4      val _ =
     5.5        Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
     5.6          build_session args
     5.7 -      handle exn => (List.app (error_message o #2) (Runtime.exn_messages exn); Exn.reraise exn);
     5.8 +      handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn);
     5.9      val _ = Options.reset_default ();
    5.10    in () end;
    5.11