# HG changeset patch # User nipkow # Date 1690434512 -7200 # Node ID 2e58b5a3fecff76ae8e74fd09116b207b327bbb1 # Parent 67bf692cf1ab2e02bb03bc22c1b8f83d88852a0e# Parent 7c3d681f11d43b50771fc71513a3a1e31c48764d merged diff -r 7c3d681f11d4 -r 2e58b5a3fecf .hgtags --- a/.hgtags Wed Jul 26 21:03:57 2023 +0200 +++ b/.hgtags Thu Jul 27 07:08:32 2023 +0200 @@ -42,3 +42,4 @@ 1ac2416e843293bc6917ba965f54b42962514b7f Isabelle2022 f4221ae7544ca26fdfba64d4e04ebd3d3b5a694d Isabelle2023-RC0 006dbc9c2de1d1c541a9d822b42c70fedf223e08 Isabelle2023-RC1 +53b59fa42696a6eff4bf073b510fc923794e7df5 Isabelle2023-RC2 diff -r 7c3d681f11d4 -r 2e58b5a3fecf NEWS --- a/NEWS Wed Jul 26 21:03:57 2023 +0200 +++ b/NEWS Thu Jul 27 07:08:32 2023 +0200 @@ -9,6 +9,11 @@ *** General *** +* Toplevel results --- like declared consts and proven theorems --- are +printed as regular "writeln" message instead of "state", which is no +specifically for proof states. This affects Isabelle/jEdit panels for +Output vs. State in particular. + * Session build dependencies (sources and heaps) are now recorded in more details, with one SHA1 digest per file and a symbolic version of the file name -- similar to the Unix command-line tool "sha1sum". For diff -r 7c3d681f11d4 -r 2e58b5a3fecf src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Jul 26 21:03:57 2023 +0200 +++ b/src/Pure/Isar/proof.ML Thu Jul 27 07:08:32 2023 +0200 @@ -1153,7 +1153,7 @@ val _ = (case Proof_Display.pretty_goal_inst goal_ctxt propss goal of [] => () - | prts => Output.state (Pretty.string_of (Pretty.chunks prts))); + | prts => Pretty.writeln (Pretty.chunks prts)); in result_ctxt end; fun global_qed arg = @@ -1231,7 +1231,9 @@ local fun gen_have prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int = - local_goal (Proof_Display.print_results int (Position.thread_data ())) + local_goal + (Proof_Display.print_results + {interactive = int, pos = Position.thread_data (), proof_state = true}) 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 = @@ -1246,7 +1248,7 @@ val pos = Position.thread_data (); fun print_results ctxt res = if ! testing then () - else Proof_Display.print_results int pos ctxt res; + else Proof_Display.print_results {interactive = int, pos = pos, proof_state = true} ctxt res; fun print_rule ctxt th = if ! testing then rule := SOME th else if int then diff -r 7c3d681f11d4 -r 2e58b5a3fecf src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Wed Jul 26 21:03:57 2023 +0200 +++ b/src/Pure/Isar/proof_display.ML Thu Jul 27 07:08:32 2023 +0200 @@ -24,7 +24,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: bool -> Position.T -> Proof.context -> + val print_results: {interactive: bool, pos: Position.T, proof_state: bool} -> 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 -> @@ -349,22 +349,25 @@ in -fun print_results int pos ctxt ((kind, name), facts) = - if kind = "" orelse no_print int ctxt then () - else if name = "" then - (Output.state o Pretty.string_of) - (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 :: - pretty_facts ctxt facts)) - else - (Output.state o Pretty.string_of) - (case facts of - [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk, - Proof_Context.pretty_fact ctxt fact]) - | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk, - Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])); +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 (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 :: + pretty_facts ctxt facts)) + else + print + (case facts of + [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk, + Proof_Context.pretty_fact ctxt fact]) + | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk, + Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])])) + end; fun print_theorem pos ctxt fact = - print_results true pos ctxt ((Thm.theoremK, ""), [fact]); + print_results {interactive = true, pos = pos, proof_state = false} + ctxt ((Thm.theoremK, ""), [fact]); end; @@ -393,7 +396,7 @@ fun print_consts int pos ctxt pred cs = if null cs orelse no_print int ctxt then () - else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs)); + else Pretty.writeln (pretty_consts pos ctxt pred cs); end; diff -r 7c3d681f11d4 -r 2e58b5a3fecf src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Wed Jul 26 21:03:57 2023 +0200 +++ b/src/Pure/Isar/specification.ML Thu Jul 27 07:08:32 2023 +0200 @@ -343,7 +343,10 @@ |> Attrib.partial_evaluation ctxt' |> Attrib.transform_facts (Proof_Context.export_morphism ctxt' lthy); val (res, lthy') = lthy |> Local_Theory.notes_kind kind facts'; - val _ = Proof_Display.print_results int (Position.thread_data ()) lthy' ((kind, ""), res); + val _ = + Proof_Display.print_results + {interactive = int, pos = Position.thread_data (), proof_state = false} + lthy' ((kind, ""), res); in (res, lthy') end; in @@ -396,6 +399,9 @@ 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}; + fun after_qed' results goal_ctxt' = let val results' = @@ -406,13 +412,13 @@ Local_Theory.notes_kind kind (map2 (fn (b, _) => fn ths => (b, [(ths, [])])) stmt results') lthy; val lthy'' = - if Binding.is_empty_atts (name, atts) then - (Proof_Display.print_results int pos lthy' ((kind, ""), res); lthy') + if Binding.is_empty_atts (name, atts) + then (print_results lthy' ((kind, ""), res); lthy') else let val ([(res_name, _)], lthy'') = Local_Theory.notes_kind kind [((name, atts), [(maps #2 res, [])])] lthy'; - val _ = Proof_Display.print_results int pos lthy' ((kind, res_name), res); + val _ = print_results lthy' ((kind, res_name), res); in lthy'' end; in after_qed results' lthy'' end; diff -r 7c3d681f11d4 -r 2e58b5a3fecf src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Jul 26 21:03:57 2023 +0200 +++ b/src/Pure/Isar/toplevel.ML Thu Jul 27 07:08:32 2023 +0200 @@ -456,7 +456,7 @@ val _ = (case Local_Theory.pretty lthy of [] => () - | prts => Output.state (Pretty.string_of (Pretty.chunks prts))); + | prts => Pretty.writeln (Pretty.chunks prts)); in (Theory gthy, lthy) end | _ => raise UNDEF)); diff -r 7c3d681f11d4 -r 2e58b5a3fecf src/Pure/ex/Guess.thy --- a/src/Pure/ex/Guess.thy Wed Jul 26 21:03:57 2023 +0200 +++ b/src/Pure/ex/Guess.thy Thu Jul 27 07:08:32 2023 +0200 @@ -149,7 +149,8 @@ val goal = Var guess; val pos = Position.thread_data (); fun print_result ctxt' (k, [(s, [_, th])]) = - Proof_Display.print_results int pos ctxt' (k, [(s, [th])]); + Proof_Display.print_results {interactive = int, pos = pos, proof_state = true} + ctxt' (k, [(s, [th])]); val before_qed = Method.primitive_text (fn ctxt => Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>