equal
deleted
inserted
replaced
32 Isabelle2015). |
32 Isabelle2015). |
33 |
33 |
34 |
34 |
35 *** Prover IDE -- Isabelle/Scala/jEdit *** |
35 *** Prover IDE -- Isabelle/Scala/jEdit *** |
36 |
36 |
37 * IDE support for the Isabelle/Pure bootstrap process. The initial files |
37 * IDE support for the Isabelle/Pure bootstrap process, with the |
38 src/Pure/ROOT0.ML or src/Pure/ROOT.ML may be opened with Isabelle/jEdit: |
38 following independent stages: |
39 they act like independent quasi-theories in the context of theory |
39 |
40 ML_Bootstrap. This allows continuous checking of ML files as usual, but |
40 src/Pure/ROOT0.ML |
41 results are isolated from the actual Isabelle/Pure that runs the IDE |
41 src/Pure/ROOT.ML |
42 itself. |
42 src/Pure/Pure.thy |
|
43 src/Pure/ML_Bootstrap.thy |
|
44 |
|
45 The ML ROOT files act like quasi-theories in the context of theory |
|
46 ML_Bootstrap: this allows continuous checking of all loaded ML files. |
|
47 The theory files are presented with a modified header to import Pure |
|
48 from the running Isabelle instance. Results from changed versions of |
|
49 each stage are *not* propagated to the next stage, and isolated from the |
|
50 actual Isabelle/Pure that runs the IDE itself. The sequential |
|
51 dependencies of the above files are only relevant for batch build. |
43 |
52 |
44 * Highlighting of entity def/ref positions wrt. cursor. |
53 * Highlighting of entity def/ref positions wrt. cursor. |
45 |
54 |
46 |
55 |
47 *** Isar *** |
56 *** Isar *** |