TODO.md
author wenzelm
Mon, 19 Apr 2021 20:31:24 +0200
changeset 60238 f451e3426955
parent 60234 0d35baf1108e
child 60241 07849bde0c95
permissions -rw-r--r--
done;
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;