--- 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
--- 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
--- 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 \<open>Checking the index maximum for \<text>\<open>PolyML\<close>\<close>
+text \<open>Checking the index maximum for \<^verbatim>\<open>PolyML\<close>.\<close>
qualified definition \<open>check_max = ()\<close>
--- 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 =
--- 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;
--- 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;
--- 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 "" = ""
--- 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 ());
--- 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;
--- 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;
--- 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;
--- /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;