equal
deleted
inserted
replaced
38 automatically. |
38 automatically. |
39 |
39 |
40 * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation') |
40 * ML setup commands (e.g. 'setup', 'method_setup', 'parse_translation') |
41 need to provide a closed expression -- without trailing semicolon. Minor |
41 need to provide a closed expression -- without trailing semicolon. Minor |
42 INCOMPATIBILITY. |
42 INCOMPATIBILITY. |
|
43 |
|
44 * Commands 'generate_file', 'export_generated_files', and |
|
45 'compile_generated_files' support a stateless (PIDE-conformant) model |
|
46 for generated sources and compiled binaries of other languages. The |
|
47 compilation processed is managed in Isabelle/ML, and results exported to |
|
48 the session database for further use (e.g. with "isabelle export" or |
|
49 "isabelle build -e"). |
43 |
50 |
44 |
51 |
45 *** Isabelle/jEdit Prover IDE *** |
52 *** Isabelle/jEdit Prover IDE *** |
46 |
53 |
47 * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle |
54 * Fonts for the text area, gutter, GUI elements etc. use the "Isabelle |