equal
deleted
inserted
replaced
457 ML_Context.antiquotation and structure ML_Antiquotation. Minor |
457 ML_Context.antiquotation and structure ML_Antiquotation. Minor |
458 INCOMPATIBILITY. |
458 INCOMPATIBILITY. |
459 |
459 |
460 * ML antiquotation @{here} refers to its source position, which is |
460 * ML antiquotation @{here} refers to its source position, which is |
461 occasionally useful for experimentation and diagnostic purposes. |
461 occasionally useful for experimentation and diagnostic purposes. |
|
462 |
|
463 * ML antiquotation @{path} produces a Path.T value, similarly to |
|
464 Path.explode, but with compile-time check against the file-system and |
|
465 some PIDE markup. Note that unlike theory source, ML does not have a |
|
466 well-defined master directory, so an absolute symbolic path |
|
467 specification is usually required, e.g. "~~/src/HOL". |
462 |
468 |
463 |
469 |
464 *** System *** |
470 *** System *** |
465 |
471 |
466 * Simplified "isabelle display" tool. Settings variables DVI_VIEWER |
472 * Simplified "isabelle display" tool. Settings variables DVI_VIEWER |