TODO.md
author wenzelm
Mon, 19 Apr 2021 13:57:47 +0200
changeset 60229 5d05ad9c80df
parent 60225 36cad744ecb9
child 60234 0d35baf1108e
permissions -rw-r--r--
more TODO;
     1 * WN: check remaining "for tests only" wrt. \<^isac_test>CARTOUCHE;
     2 
     3 * WN: eliminate "handle _ => ..." (essential for PIDE interaction):
     4     - either use \<^try>CARTOUCHE / \<^can>CARTOUCHE antiquotation
     5     - or more basic try/can combinators;
     6 
     7 * WN: eliminate odd notation term tricks: replace "^^^" e.g. by "\<up>" based on "_ powr _" for type real;
     8 
     9 * WN: eliminate ThmC.numerals_to_Free, use existing Isabelle/HOL representation;
    10 
    11 * MW: clarify/eliminate Isabelle/Scala add-ons (presently unused)
    12 
    13     diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/build-jars ./src/Pure/build-jars
    14     11a12
    15     >   src/Tools/isac/BridgeJEdit/isac.scala
    16 
    17     diff -r /home/makarius/isabelle/repos-Isabelle2021/src/Pure/Tools/scala_project.scala ./src/Pure/Tools/scala_project.scala
    18     76a77
    19     >       "src/Tools/isac/etc" -> Path.explode("isabelle.isac"),
    20 
    21 * reconsider use of Thy_Info.get_theory: only works with batch-build, not within PIDE session;
    22 
    23 * MW: check uses of Unsynchronized.ref vs. Synchronized.var;