| 2012-02-18 |
haftmann |
avoid redefinition of @{theory} antiquotation
|
file |
diff |
annotate
|
| 2012-02-18 |
haftmann |
more precise semantics of "theory" antiquotation
|
file |
diff |
annotate
|
| 2012-01-25 |
wenzelm |
document antiquotations for ML infix operators;
|
file |
diff |
annotate
|
| 2011-11-29 |
bulwahn |
adjusting antiquote_setup (cf. d83797ef0d2d)
|
file |
diff |
annotate
|
| 2011-06-27 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| 2011-06-27 |
wenzelm |
proper checking of @{ML_antiquotation};
|
file |
diff |
annotate
|
| 2011-05-03 |
wenzelm |
use existing \<hyphen>;
|
file |
diff |
annotate
|
| 2011-04-16 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| 2011-04-08 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| 2010-11-29 |
wenzelm |
added document antiquotation @{file};
|
file |
diff |
annotate
|
| 2010-10-19 |
wenzelm |
more robust treatment of "op IDENT";
|
file |
diff |
annotate
|
| 2010-10-19 |
wenzelm |
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
|
file |
diff |
annotate
|
| 2010-10-16 |
wenzelm |
more robust treatment of symbolic indentifiers (which may contain colons);
|
file |
diff |
annotate
|
| 2010-10-08 |
wenzelm |
more on ML antiquotations;
|
file |
diff |
annotate
|
| 2010-08-27 |
wenzelm |
proper context for various Thy_Output options, via official configuration options in ML and Isar;
|
file |
diff |
annotate
|
| 2010-07-27 |
wenzelm |
updated manual concerning theory loader;
|
file |
diff |
annotate
|
| 2010-05-31 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| 2010-05-30 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|
| 2010-05-18 |
wenzelm |
prefer structure Keyword and Parse;
|
file |
diff |
annotate
|
| 2010-04-16 |
wenzelm |
proper checking of ML functors (in Poly/ML 5.2 or later);
|
file |
diff |
annotate
|
| 2009-06-10 |
wenzelm |
eliminated escaped symbols;
|
file |
diff |
annotate
|
| 2009-05-30 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2009-03-09 |
wenzelm |
fornal markup for antiquotation options;
|
file |
diff |
annotate
|
| 2009-03-09 |
wenzelm |
moved @{ML_functor} and @{ML_text} to Pure;
|
file |
diff |
annotate
|
| 2009-03-09 |
wenzelm |
adapted ThyOutput.antiquotation;
|
file |
diff |
annotate
|
| 2009-03-08 |
wenzelm |
use simplified ThyOutput.antiquotation;
|
file |
diff |
annotate
|
| 2009-03-08 |
wenzelm |
adapted to structure Long_Name;
|
file |
diff |
annotate
|
| 2009-03-08 |
wenzelm |
index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
|
file |
diff |
annotate
|
| 2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| 2009-03-04 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| 2009-02-26 |
wenzelm |
uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
|
file |
diff |
annotate
|
| 2009-02-14 |
wenzelm |
clean_string/clean_name: proper treatment of \<dash>;
|
file |
diff |
annotate
|
| 2009-02-11 |
wenzelm |
added "inference" entity;
|
file |
diff |
annotate
|
| 2008-11-13 |
wenzelm |
ignore ThyOutput.source flag;
|
file |
diff |
annotate
|
| 2008-10-21 |
wenzelm |
ThyOutput: export some auxiliary operations;
|
file |
diff |
annotate
|
| 2008-09-29 |
haftmann |
added theory antiquotation
|
file |
diff |
annotate
|
| 2008-09-17 |
wenzelm |
simplified ML_Context.eval_in -- expect immutable Proof.context value;
|
file |
diff |
annotate
|
| 2008-09-16 |
wenzelm |
check setting and tool;
|
file |
diff |
annotate
|
| 2008-09-15 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| 2008-09-15 |
wenzelm |
added formal markup for setting, executable, tool;
|
file |
diff |
annotate
|
| 2008-08-09 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
file |
diff |
annotate
|
| 2008-06-25 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
| 2008-05-15 |
wenzelm |
tuned clean_name (underscore);
|
file |
diff |
annotate
|
| 2008-05-15 |
wenzelm |
clean_name: replace "_" by "-";
|
file |
diff |
annotate
|
| 2008-05-15 |
wenzelm |
clean_string: cover <;
|
file |
diff |
annotate
|
| 2008-05-14 |
wenzelm |
proper checking of various Isar elements;
|
file |
diff |
annotate
|
| 2008-05-08 |
wenzelm |
clean_string: map "_" to "\\_" (best used with underscore.sty);
|
file |
diff |
annotate
|
| 2008-05-07 |
wenzelm |
output_entity: ignore ThyOutput.source option;
|
file |
diff |
annotate
|
| 2008-05-05 |
wenzelm |
element: isakeyword markup;
|
file |
diff |
annotate
|
| 2008-05-02 |
wenzelm |
output_entity: added \mbox{} to prevent hyphenation;
|
file |
diff |
annotate
|
| 2008-05-02 |
wenzelm |
clean_string: handle { };
|
file |
diff |
annotate
|
| 2008-04-28 |
wenzelm |
proper command/keyword markup;
|
file |
diff |
annotate
|
| 2008-04-26 |
wenzelm |
added setup for Isar entities;
|
file |
diff |
annotate
|
| 2008-04-23 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| 2008-04-17 |
wenzelm |
pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
|
file |
diff |
annotate
|
| 2008-03-28 |
haftmann |
some styling
|
file |
diff |
annotate
|
| 2008-03-27 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
| 2008-03-24 |
wenzelm |
ML runtime compilation: pass position, tuned signature;
|
file |
diff |
annotate
|
| 2007-10-08 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| 2007-09-15 |
haftmann |
fixed title
|
file |
diff |
annotate
|