# HG changeset patch # User wenzelm # Date 1745530197 -7200 # Node ID 7ab0fb5d9919f59d49ef0dfe8d40d0b0cfd77b20 # Parent cf21066637d7f6a6e9996ecbfed567de7b4d253c# Parent abd3885a3fcffbe45b2138d2f0a638cb103f54c9 merged diff -r cf21066637d7 -r 7ab0fb5d9919 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Apr 24 15:29:48 2025 +0200 +++ b/Admin/components/components.sha1 Thu Apr 24 23:29:57 2025 +0200 @@ -274,6 +274,7 @@ 23297ab36a853247a17f87b94a29654f3259b341 jedit-20250417.tar.gz a291746959e64916e8504b89dca804186d4eb8a1 jedit-20250422.tar.gz 07360418d691f6bb0e250e8efeb6b935e23eb0cd jedit-20250423.tar.gz +995ac4cd9086e1647f1628988884c7c135123965 jedit-20250424.tar.gz 44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz 4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz diff -r cf21066637d7 -r 7ab0fb5d9919 Admin/components/main --- a/Admin/components/main Thu Apr 24 15:29:48 2025 +0200 +++ b/Admin/components/main Thu Apr 24 23:29:57 2025 +0200 @@ -15,7 +15,7 @@ isabelle_setup-20240327 javamail-20250122 jdk-21.0.6 -jedit-20250423 +jedit-20250424 jfreechart-1.5.3 jortho-1.0-2 jsoup-1.18.3 diff -r cf21066637d7 -r 7ab0fb5d9919 src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy --- a/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy Thu Apr 24 15:29:48 2025 +0200 +++ b/src/HOL/Codegenerator_Test/Generate_Target_Bit_Operations.thy Thu Apr 24 23:29:57 2025 +0200 @@ -59,7 +59,7 @@ test_code check in Scala -text \Checking the index maximum for \\PolyML\\ +text \Checking the index maximum for \<^verbatim>\PolyML\.\ qualified definition \check_max = ()\ diff -r cf21066637d7 -r 7ab0fb5d9919 src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Thu Apr 24 15:29:48 2025 +0200 +++ b/src/Pure/General/pretty.ML Thu Apr 24 23:29:57 2025 +0200 @@ -87,6 +87,7 @@ val output: output_ops -> T -> Bytes.T val string_of_ops: output_ops -> T -> string val string_of: T -> string + val strings_of: T -> string list val pure_string_of: T -> string val writeln: T -> unit val writeln_urgent: T -> unit @@ -527,6 +528,8 @@ fun string_of_ops ops = Bytes.content o output ops; fun string_of prt = string_of_ops (output_ops NONE) prt; +fun strings_of prt = Bytes.contents (output (output_ops NONE) prt); + val pure_string_of = string_of_ops (pure_output_ops NONE); fun gen_writeln urgent prt = diff -r cf21066637d7 -r 7ab0fb5d9919 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Thu Apr 24 15:29:48 2025 +0200 +++ b/src/Pure/Isar/calculation.ML Thu Apr 24 23:29:57 2025 +0200 @@ -160,7 +160,7 @@ if int then Proof_Context.pretty_fact ctxt' (Proof_Context.full_name ctxt' (Binding.name calculationN), calc) - |> Pretty.string_of |> writeln + |> Pretty.writeln else (); in state' |> final ? (update_calculation NONE #> Proof.chain_facts calc) end; diff -r cf21066637d7 -r 7ab0fb5d9919 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Apr 24 15:29:48 2025 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Apr 24 23:29:57 2025 +0200 @@ -244,55 +244,53 @@ local -fun string_of_stmts ctxt args = +fun pretty_stmts ctxt args = Attrib.eval_thms ctxt args |> map (Element.pretty_statement ctxt Thm.theoremK) - |> Pretty.chunks2 |> Pretty.string_of; + |> Pretty.chunks2; -fun string_of_thms ctxt args = - Pretty.string_of (Proof_Context.pretty_fact ctxt ("", Attrib.eval_thms ctxt args)); +fun pretty_thms ctxt args = + Proof_Context.pretty_fact ctxt ("", Attrib.eval_thms ctxt args); -fun string_of_prfs full state arg = - Pretty.string_of - (case arg of - NONE => - let - val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); - val thy = Proof_Context.theory_of ctxt; - val prf = Thm.proof_of thm; - val prop = Thm.full_prop_of thm; - val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; - in - Proof_Syntax.pretty_proof ctxt - (if full then Proofterm.reconstruct_proof thy prop prf' else prf') - end - | SOME srcs => - let - val ctxt = Toplevel.context_of state; - val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full; - in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end); +fun pretty_prfs full state arg = + (case arg of + NONE => + let + val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state); + val thy = Proof_Context.theory_of ctxt; + val prf = Thm.proof_of thm; + val prop = Thm.full_prop_of thm; + val prf' = Proofterm.rewrite_proof_notypes ([], []) prf; + in + Proof_Syntax.pretty_proof ctxt + (if full then Proofterm.reconstruct_proof thy prop prf' else prf') + end + | SOME srcs => + let + val ctxt = Toplevel.context_of state; + val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full; + in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end); -fun string_of_prop ctxt s = +fun pretty_prop ctxt s = let val prop = Syntax.read_prop ctxt s; val ctxt' = Proof_Context.augment prop ctxt; - in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end; + in Pretty.quote (Syntax.pretty_term ctxt' prop) end; -fun string_of_term ctxt s = +fun pretty_term ctxt s = let val t = Syntax.read_term ctxt s; val T = Term.type_of t; val ctxt' = Proof_Context.augment t ctxt; in - Pretty.string_of - (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, - Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]) + Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk, + Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)] end; -fun string_of_type ctxt (s, NONE) = +fun pretty_type ctxt (s, NONE) = let val T = Syntax.read_typ ctxt s - in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end - | string_of_type ctxt (s1, SOME s2) = + in Pretty.quote (Syntax.pretty_typ ctxt T) end + | pretty_type ctxt (s1, SOME s2) = let val ctxt' = Config.put show_sorts true ctxt; val raw_T = Syntax.parse_typ ctxt' s1; @@ -301,19 +299,19 @@ Syntax.check_term ctxt' (Logic.mk_type raw_T |> Type.constraint (Term.itselfT (Type_Infer.anyT S))) |> Logic.dest_type; - in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end; + in Pretty.quote (Syntax.pretty_typ ctxt' T) end; -fun print_item string_of (modes, arg) = Toplevel.keep (fn state => - Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ()); +fun print_item pretty (modes, arg) = Toplevel.keep (fn state => + Print_Mode.with_modes modes (fn () => Pretty.writeln (pretty state arg)) ()); in -val print_stmts = print_item (string_of_stmts o Toplevel.context_of); -val print_thms = print_item (string_of_thms o Toplevel.context_of); -val print_prfs = print_item o string_of_prfs; -val print_prop = print_item (string_of_prop o Toplevel.context_of); -val print_term = print_item (string_of_term o Toplevel.context_of); -val print_type = print_item (string_of_type o Toplevel.context_of); +val print_stmts = print_item (pretty_stmts o Toplevel.context_of); +val print_thms = print_item (pretty_thms o Toplevel.context_of); +val print_prfs = print_item o pretty_prfs; +val print_prop = print_item (pretty_prop o Toplevel.context_of); +val print_term = print_item (pretty_term o Toplevel.context_of); +val print_type = print_item (pretty_type o Toplevel.context_of); end; diff -r cf21066637d7 -r 7ab0fb5d9919 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Thu Apr 24 15:29:48 2025 +0200 +++ b/src/Pure/PIDE/markup.ML Thu Apr 24 23:29:57 2025 +0200 @@ -293,6 +293,7 @@ val no_output: output val output: T -> output val markup: T -> string -> string + val markup_strings: T -> string list -> string list val markups: T list -> string -> string val markup_report: string -> string end; @@ -898,6 +899,10 @@ fun markup m = output m |-> Library.enclose; +fun markup_strings m = + let val (bg, en) = output m + in fn ss => [bg] @ ss @ [en] end; + val markups = fold_rev markup; fun markup_report "" = "" diff -r cf21066637d7 -r 7ab0fb5d9919 src/Pure/PIDE/query_operation.ML --- a/src/Pure/PIDE/query_operation.ML Thu Apr 24 15:29:48 2025 +0200 +++ b/src/Pure/PIDE/query_operation.ML Thu Apr 24 23:29:57 2025 +0200 @@ -9,7 +9,9 @@ sig val register: {name: string, pri: int} -> ({state: Toplevel.state, args: string list, - output_result: string -> unit, writeln_result: string -> unit} -> unit) -> unit + output_result: string list -> unit, + writelns_result: string list -> unit, + writeln_result: string -> unit} -> unit) -> unit end; structure Query_Operation: QUERY_OPERATION = @@ -21,16 +23,17 @@ SOME {delay = NONE, pri = pri, persistent = false, strict = false, print_fn = fn _ => Thread_Attributes.uninterruptible (fn run => fn state => let - fun output_result s = Output.result [(Markup.instanceN, instance)] [s]; - fun status m = output_result (YXML.output_markup_only m); - fun writeln_result s = output_result (Markup.markup Markup.writeln s); + fun output_result ss = Output.result [(Markup.instanceN, instance)] ss; + fun status m = output_result [YXML.output_markup_only m]; + fun writelns_result ss = output_result (Markup.markup_strings Markup.writeln ss); + val writeln_result = writelns_result o single; fun toplevel_error exn = - output_result (Markup.markup Markup.error (Runtime.exn_message exn)); + output_result [Markup.markup Markup.error (Runtime.exn_message exn)]; val _ = status Markup.running; fun main () = f {state = state, args = args, output_result = output_result, - writeln_result = writeln_result}; + writelns_result = writelns_result, writeln_result = writeln_result}; val _ = (case Exn.capture_body (*sic!*) (run main) of Exn.Res () => () @@ -47,5 +50,10 @@ Query_Operation.register {name = "print_state", pri = Task_Queue.urgent_pri} (fn {state = st, output_result, ...} => if Toplevel.is_proof st - then output_result (Markup.markup Markup.state (Toplevel.string_of_state st)) + then + Toplevel.pretty_state st + |> Pretty.chunks + |> Pretty.strings_of + |> Markup.markup_strings Markup.state + |> output_result else ()); diff -r cf21066637d7 -r 7ab0fb5d9919 src/Pure/Tools/find_consts.ML --- a/src/Pure/Tools/find_consts.ML Thu Apr 24 15:29:48 2025 +0200 +++ b/src/Pure/Tools/find_consts.ML Thu Apr 24 23:29:57 2025 +0200 @@ -159,13 +159,13 @@ val _ = Query_Operation.register {name = "find_consts", pri = Task_Queue.urgent_pri} - (fn {state, args, writeln_result, ...} => + (fn {state, args, writelns_result, ...} => (case try Toplevel.context_of state of SOME ctxt => let val [query_arg] = args; val query = read_query Position.none query_arg; - in writeln_result (Pretty.string_of (pretty_consts ctxt query)) end + in writelns_result (Pretty.strings_of (pretty_consts ctxt query)) end | NONE => error "Unknown context")); end; diff -r cf21066637d7 -r 7ab0fb5d9919 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Thu Apr 24 15:29:48 2025 +0200 +++ b/src/Pure/Tools/find_theorems.ML Thu Apr 24 23:29:57 2025 +0200 @@ -536,7 +536,7 @@ val _ = Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri} - (fn {state = st, args, writeln_result, ...} => + (fn {state = st, args, writelns_result, ...} => if can Toplevel.context_of st then let val [limit_arg, allow_dups_arg, query_arg] = args; @@ -544,7 +544,7 @@ val opt_limit = Int.fromString limit_arg; val rem_dups = allow_dups_arg = "false"; val criteria = read_query Position.none query_arg; - in writeln_result (Pretty.string_of (pretty_theorems state opt_limit rem_dups criteria)) end + in writelns_result (Pretty.strings_of (pretty_theorems state opt_limit rem_dups criteria)) end else error "Unknown context"); end; diff -r cf21066637d7 -r 7ab0fb5d9919 src/Pure/Tools/print_operation.ML --- a/src/Pure/Tools/print_operation.ML Thu Apr 24 15:29:48 2025 +0200 +++ b/src/Pure/Tools/print_operation.ML Thu Apr 24 23:29:57 2025 +0200 @@ -40,7 +40,7 @@ val _ = Query_Operation.register {name = "print_operation", pri = Task_Queue.urgent_pri} - (fn {state, args, writeln_result, ...} => + (fn {state, args, writelns_result, ...} => let val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context"; fun err s = Pretty.mark_str (Markup.bad (), s); @@ -48,7 +48,7 @@ (case AList.lookup (op =) (Synchronized.value print_operations) name of SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"]) | NONE => [err ("Unknown print operation: " ^ quote name)]); - in writeln_result (Pretty.string_of (Pretty.chunks (maps print args))) end); + in writelns_result (Pretty.strings_of (Pretty.chunks (maps print args))) end); end; diff -r cf21066637d7 -r 7ab0fb5d9919 src/Tools/jEdit/patches/position_changing --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/patches/position_changing Thu Apr 24 23:29:57 2025 +0200 @@ -0,0 +1,24 @@ +diff -ru jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java +--- jedit5.7.0/jEdit/org/gjt/sp/jedit/EditPane.java 2024-08-03 19:53:15.000000000 +0200 ++++ jedit5.7.0-patched/jEdit/org/gjt/sp/jedit/EditPane.java 2025-04-24 11:45:26.809862122 +0200 +@@ -43,6 +43,7 @@ + import org.gjt.sp.jedit.msg.BufferChanging; + import org.gjt.sp.jedit.msg.BufferUpdate; + import org.gjt.sp.jedit.msg.EditPaneUpdate; ++import org.gjt.sp.jedit.msg.PositionChanging; + import org.gjt.sp.jedit.msg.PropertiesChanged; + import org.gjt.sp.jedit.options.GeneralOptionPane; + import org.gjt.sp.jedit.options.GutterOptionPane; +@@ -380,9 +381,11 @@ + buffer.unsetProperty(Buffer.CARET_POSITIONED); + + +- if(caret != -1) ++ if(caret != -1) { + textArea.setCaretPosition(Math.min(caret, + buffer.getLength())); ++ EditBus.send(new PositionChanging(this)); ++ } + + // set any selections + Selection[] selection = caretInfo.selection;