Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. no view_document after build: avoid loss of focus, especially in "auto build" mode;
  2. tuned message;
  3. build only if required, view only after proper build: thus avoid pointless events in "auto build" mode;
  4. clarified modules;
  5. maintain document_output meta data;
  6. clarified modules;
  7. avoid redundant SelectionChanged events;
  8. more logging;
  9. proper symbolic handle on component resources: diff -r ci-extras-1/etc/settings ci-extras-2/etc/settings 1c1,4 < classpath "$COMPONENT/lib/ci-extras.jar" --- > #-*- shell-script -*- :mode=shellscript: > > ISABELLE_CI_EXTRAS_JAR="$COMPONENT/lib/ci-extras.jar" > classpath "$ISABELLE_CI_EXTRAS_JAR" diff -r ci-extras-1/README ci-extras-2/README 11a12 > Makarius, 02-Feb-2023
  10. more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);
Changeset 77189:461c078e545f by wenzelm:
no view_document after build: avoid loss of focus, especially in &quot;auto build&quot; mode;
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
Changeset 77188:608668d39689 by wenzelm:
tuned message;
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
Changeset 77187:628a34f4f754 by wenzelm:
build only if required, view only after proper build: thus avoid pointless events in &quot;auto build&quot; mode;
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
Changeset 77186:68d8ff348941 by wenzelm:
clarified modules;
The file was modified src/Pure/Thy/document_build.scala (diff)
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
Changeset 77185:9dc4d9ed886f by wenzelm:
maintain document_output meta data;
The file was modified src/Pure/General/path.scala (diff)
The file was modified src/Pure/PIDE/document_editor.scala (diff)
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
Changeset 77184:861777e58b77 by wenzelm:
clarified modules;
The file was modified src/Pure/PIDE/document_editor.scala (diff)
The file was modified src/Tools/jEdit/src/document_dockable.scala (diff)
Changeset 77183:45b9bbe6e375 by wenzelm:
avoid redundant SelectionChanged events;
The file was modified src/Tools/jEdit/src/jedit_sessions.scala (diff)
Changeset 77182:25dbf5bec91e by wenzelm:
more logging;
The file was modified src/Pure/Concurrent/delay.scala (diff)
The file was modified src/Pure/General/logger.scala (diff)
Changeset 77181:3eb3de867786 by wenzelm:
proper symbolic handle on component resources:<br>diff -r ci-extras-1/etc/settings ci-extras-2/etc/settings<br>1c1,4<br>&lt; classpath &quot;$COMPONENT/lib/ci-extras.jar&quot;<br>---<br>&gt; #-*- shell-script -*- :mode=shellscript:<br>&gt;<br>&gt; ISABELLE_CI_EXTRAS_JAR=&quot;$COMPONENT/lib/ci-extras.jar&quot;<br>&gt; classpath &quot;$ISABELLE_CI_EXTRAS_JAR&quot;<br>diff -r ci-extras-1/README ci-extras-2/README<br>11a12<br>&gt; Makarius, 02-Feb-2023
The file was modified Admin/components/components.sha1 (diff)
Changeset 77180:7af930cd0fce by wenzelm:
more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);
The file was modified src/Pure/General/file.ML (diff)