author | wenzelm |
Mon, 19 Apr 2021 20:31:24 +0200 | |
changeset 60238 | f451e3426955 |
parent 60234 | 0d35baf1108e |
child 60241 | 07849bde0c95 |
permissions | -rw-r--r-- |
wenzelm@60219 | 1 |
* WN: eliminate "handle _ => ..." (essential for PIDE interaction): |
wenzelm@60219 | 2 |
- either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation |
wenzelm@60219 | 3 |
- or more basic try/can combinators; |
wenzelm@60234 | 4 |
- or more direct ML of intention; |
wenzelm@60216 | 5 |
|
wenzelm@60234 | 6 |
* WN: check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE; |
wenzelm@60219 | 7 |
|
wenzelm@60234 | 8 |
* WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>" |
wenzelm@60234 | 9 |
based on "_ powr _" for type real; |
wenzelm@60234 | 10 |
|
wenzelm@60234 | 11 |
abbreviation real_powr :: "real \<Rightarrow> real \<Rightarrow> real" (infixr "\<up>" 80) |
wenzelm@60234 | 12 |
where "x \<up> a \<equiv> x powr a" |
wenzelm@60234 | 13 |
|
wenzelm@60234 | 14 |
* WN: purge BridgeLibisabelle: eliminate unused code; |
wenzelm@60234 | 15 |
|
wenzelm@60234 | 16 |
|
wenzelm@60234 | 17 |
* reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session; |
wenzelm@60234 | 18 |
|
wenzelm@60234 | 19 |
|
wenzelm@60234 | 20 |
* MW: check JVM resource requirements of session Isac_Test; |
wenzelm@60234 | 21 |
|
wenzelm@60234 | 22 |
* MW: check uses of Unsynchronized.ref vs. Synchronized.var; |
wenzelm@60234 | 23 |
|
wenzelm@60234 | 24 |
* MW: proper formal name space for rule set, model patterns, methods; |
wenzelm@60234 | 25 |
proper setup command; |
wenzelm@60216 | 26 |
|
wenzelm@60216 | 27 |
* MW: clarify/eliminate Isabelle/Scala add-ons (presently unused) |
wenzelm@60216 | 28 |
|
wenzelm@60216 | 29 |
diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/build-jars ./src/Pure/build-jars |
wenzelm@60216 | 30 |
11a12 |
wenzelm@60216 | 31 |
> src/Tools/isac/BridgeJEdit/isac.scala |
wenzelm@60216 | 32 |
|
wenzelm@60216 | 33 |
diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/Tools/scala_project.scala ./src/Pure/Tools/scala_project.scala |
wenzelm@60216 | 34 |
76a77 |
wenzelm@60216 | 35 |
> "src/Tools/isac/etc" -> Path.explode("isabelle.isac"), |
wenzelm@60225 | 36 |
|
wenzelm@60229 | 37 |
|
wenzelm@60234 | 38 |
* more direct logical foundations wrt. Isabelle/HOL, eliminate many axiomatizations; |
wenzelm@60234 | 39 |
|
wenzelm@60234 | 40 |
* WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation; |