more uniform Proof_Display.print_results for theory and proof output --- avoid loss of information seen in src/Doc/JEdit/document/output-and-state.png (the first bad changeset is f8c412a45af8, see also 53b59fa42696);
--- a/NEWS Fri Mar 21 18:37:05 2025 +0100
+++ b/NEWS Fri Mar 21 22:26:18 2025 +0100
@@ -7,6 +7,16 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Isar proof results --- notably from finished 'have' or 'show' --- are
+printed as regular "writeln" message instead of "state": this follows
+toplevel results from Isabelle2023. The order of output messages has
+been fine-tuned accordingly, to show results as "urgent" message before
+state output (if enabled). This affects Isabelle/jEdit panels for Output
+vs. State in particular.
+
+
*** HOL ***
* Theory "HOL.Fun":
--- a/src/HOL/Library/simps_case_conv.ML Fri Mar 21 18:37:05 2025 +0100
+++ b/src/HOL/Library/simps_case_conv.ML Fri Mar 21 22:26:18 2025 +0100
@@ -117,8 +117,7 @@
val thm = Attrib.eval_thms lthy thms_ref |> to_case lthy
val (res, lthy') = Local_Theory.note (bind', [thm]) lthy
val _ =
- Proof_Display.print_results
- {interactive = int, pos = Position.thread_data (), proof_state = false}
+ Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
lthy' ((Thm.theoremK, ""), [res])
in lthy' end
@@ -131,8 +130,7 @@
else gen_to_simps lthy (Attrib.eval_thms lthy splits_ref) thm
val (res, lthy') = Local_Theory.note (bind', simps) lthy
val _ =
- Proof_Display.print_results
- {interactive = int, pos = Position.thread_data (), proof_state = false}
+ Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
lthy' ((Thm.theoremK, ""), [res])
in lthy' end
--- a/src/HOL/Tools/inductive.ML Fri Mar 21 18:37:05 2025 +0100
+++ b/src/HOL/Tools/inductive.ML Fri Mar 21 22:26:18 2025 +0100
@@ -617,8 +617,7 @@
args thmss;
val (res, lthy') = lthy |> Local_Theory.notes facts
val _ =
- Proof_Display.print_results
- {interactive = int, pos = Position.thread_data (), proof_state = false}
+ Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
lthy' ((Thm.theoremK, ""), res);
in (res, lthy') end;
@@ -680,8 +679,7 @@
map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
val (res, lthy') = lthy |> Local_Theory.notes facts
val _ =
- Proof_Display.print_results
- {interactive = int, pos = Position.thread_data (), proof_state = false}
+ Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
lthy' ((Thm.theoremK, ""), res)
in (res, lthy') end;
--- a/src/Pure/Isar/proof.ML Fri Mar 21 18:37:05 2025 +0100
+++ b/src/Pure/Isar/proof.ML Fri Mar 21 22:26:18 2025 +0100
@@ -1231,8 +1231,7 @@
fun gen_have prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int =
local_goal
- (Proof_Display.print_results
- {interactive = int, pos = Position.thread_data (), proof_state = true})
+ (Proof_Display.print_results {interactive = int, pos = Position.thread_data ()})
prep_statement prep_att strict_asm "have" before_qed after_qed fixes assumes shows;
fun gen_show prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int state =
@@ -1244,16 +1243,15 @@
(case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
|> cat_lines;
- val pos = Position.thread_data ();
fun print_results ctxt res =
if ! testing then ()
- else Proof_Display.print_results {interactive = int, pos = pos, proof_state = true} ctxt res;
+ else Proof_Display.print_results {interactive = int, pos = Position.thread_data ()} ctxt res;
fun print_rule ctxt th =
if ! testing then rule := SOME th
else if int then
Proof_Display.string_of_rule ctxt "Successful" th
|> Markup.markup Markup.text_fold
- |> Output.state
+ |> Output.writeln_urgent
else ();
val test_proof =
local_skip_proof true
--- a/src/Pure/Isar/proof_display.ML Fri Mar 21 18:37:05 2025 +0100
+++ b/src/Pure/Isar/proof_display.ML Fri Mar 21 22:26:18 2025 +0100
@@ -18,7 +18,7 @@
val method_error: string -> Position.T ->
{context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
val show_results: bool Config.T
- val print_results: {interactive: bool, pos: Position.T, proof_state: bool} -> Proof.context ->
+ val print_results: {interactive: bool, pos: Position.T} -> Proof.context ->
((string * string) * (string * thm list) list) -> unit
val print_theorem: Position.T -> Proof.context -> string * thm list -> unit
val print_consts: bool -> Position.T -> Proof.context ->
@@ -317,25 +317,22 @@
in
-fun print_results {interactive, pos, proof_state} ctxt ((kind, name), facts) =
- let val print = if proof_state then Output.state o Pretty.string_of else Pretty.writeln in
- if kind = "" orelse no_print interactive ctxt then ()
- else if name = "" then
- print
- (Pretty.block (Pretty.mark_position pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
- pretty_facts ctxt facts))
- else
- print
- (case facts of
- [fact] => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk,
- Proof_Context.pretty_fact ctxt fact]
- | _ => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk,
- Pretty.block1 (Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])
- end;
+fun print_results {interactive, pos} ctxt ((kind, name), facts) =
+ if kind = "" orelse no_print interactive ctxt then ()
+ else if name = "" then
+ Pretty.writeln_urgent
+ (Pretty.block (Pretty.mark_position pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
+ pretty_facts ctxt facts))
+ else
+ Pretty.writeln_urgent
+ (case facts of
+ [fact] => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk,
+ Proof_Context.pretty_fact ctxt fact]
+ | _ => Pretty.block1 [pretty_fact_name pos (kind, name), Pretty.fbrk,
+ Pretty.block1 (Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]);
fun print_theorem pos ctxt fact =
- print_results {interactive = true, pos = pos, proof_state = false}
- ctxt ((Thm.theoremK, ""), [fact]);
+ print_results {interactive = true, pos = pos} ctxt ((Thm.theoremK, ""), [fact]);
end;
--- a/src/Pure/Isar/specification.ML Fri Mar 21 18:37:05 2025 +0100
+++ b/src/Pure/Isar/specification.ML Fri Mar 21 22:26:18 2025 +0100
@@ -344,8 +344,7 @@
|> Attrib.transform_facts (Proof_Context.export_morphism ctxt' lthy);
val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts';
val _ =
- Proof_Display.print_results
- {interactive = int, pos = Position.thread_data (), proof_state = false}
+ Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
lthy' ((kind, ""), res);
in (res, lthy') end;
@@ -398,9 +397,8 @@
|> prep_statement (prep_att lthy) prep_stmt elems raw_concl;
val atts = more_atts @ map (prep_att lthy) raw_atts;
- val pos = Position.thread_data ();
val print_results =
- Proof_Display.print_results {interactive = int, pos = pos, proof_state = false};
+ Proof_Display.print_results {interactive = int, pos = Position.thread_data ()};
fun after_qed' results goal_ctxt' =
let
--- a/src/Pure/ex/Guess.thy Fri Mar 21 18:37:05 2025 +0100
+++ b/src/Pure/ex/Guess.thy Fri Mar 21 22:26:18 2025 +0100
@@ -147,9 +147,8 @@
val guess = (("guess", 0), propT);
val goal = Var guess;
- val pos = Position.thread_data ();
fun print_result ctxt' (k, [(s, [_, th])]) =
- Proof_Display.print_results {interactive = int, pos = pos, proof_state = true}
+ Proof_Display.print_results {interactive = int, pos = Position.thread_data ()}
ctxt' (k, [(s, [th])]);
val before_qed =
Method.primitive_text (fn ctxt =>