| #
004a5084 |
|
06-Dec-2017 |
wenzelm <none@none> |
more embedded cartouche arguments;
more uniform LaTeX output for control symbols;
|
| #
401e509b |
|
13-Dec-2016 |
wenzelm <none@none> |
more symbols;
|
| #
fda5e1b6 |
|
07-Apr-2016 |
wenzelm <none@none> |
simplified default print_depth: context is usually available, in contrast to 0d295e339f52;
|
| #
2bef420f |
|
07-Apr-2016 |
wenzelm <none@none> |
clarified bootstrap of @{make_string} -- avoid query on ML environment;
|
| #
a7d79152 |
|
04-Apr-2016 |
wenzelm <none@none> |
clarified conditional compilation;
|
| #
f0caccd4 |
|
17-Mar-2016 |
wenzelm <none@none> |
@{make_string} is available during Pure bootstrap;
|
| #
54c11317 |
|
08-Dec-2014 |
wenzelm <none@none> |
expand ML cartouches to Input.source;
tuned signature;
|
| #
d65030e5 |
|
19-Aug-2014 |
wenzelm <none@none> |
tuned signature -- moved type src to Token, without aliases;
|
| #
59c73ff4 |
|
31-Jul-2014 |
wenzelm <none@none> |
clarified compile-time use of ML_print_depth;
|
| #
9e3bb39c |
|
01-May-2014 |
haftmann <none@none> |
optional case enforcement
--HG--
extra : rebase_source : 9cdeaf7fca2e9c8512cef2a7a8af271ea0daed50
|
| #
92c442b3 |
|
06-Apr-2014 |
wenzelm <none@none> |
more source positions;
|
| #
4049b387 |
|
18-Mar-2014 |
wenzelm <none@none> |
clarified modules;
more antiquotations for antiquotations;
|
| #
42ab7e1e |
|
12-Mar-2014 |
wenzelm <none@none> |
tuned signature -- clarified module name;
--HG--
rename : src/Pure/ML/ml_antiquote.ML => src/Pure/ML/ml_antiquotation.ML
|