conditional compilation via system option "isac_test" and antiquotation \<^isac_test>CARTOUCHE:
option is provided in session ROOT, or interactively via $ISABELLE_HOME_USER/etc/preferences (i.e. Isabelle/jEdit plugin preferences);
1 * WN: check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE;
3 * WN: eliminate "handle _ => ..." (essential for PIDE interaction):
4 - either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation
5 - or more basic try/can combinators;
7 * WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>" based on "_ powr _" for type real;
9 * WN: eliminate numerals_to_free, use existing Isabelle/HOL facilities;
11 * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
13 diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/build-jars ./src/Pure/build-jars
15 > src/Tools/isac/BridgeJEdit/isac.scala
17 diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/Tools/scala_project.scala ./src/Pure/Tools/scala_project.scala
19 > "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
21 * clarify test of sym_thm (and variations):
23 changeset: 60213:8b135961eb45
24 parent: 60211:b69ff7aee3f4
25 user: Walther Neuper <walther.neuper@jku.at>
26 date: Sun Apr 18 15:19:32 2021 +0200
27 files: test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml test/Tools/isac/MathEngBasic/thmC.sml
29 shift test without correction of error