#
918edcdc |
|
28-Feb-2018 |
wenzelm <none@none> |
clarified syntax: reject formal comments explicitly, instead of ignoring them silently;
|
#
ef405436 |
|
03-Feb-2018 |
wenzelm <none@none> |
more uniform treatment of formal comments within document source; more robust nesting;
|
#
ea4853ba |
|
28-Jan-2018 |
wenzelm <none@none> |
clarified take/drop/chop prefix/suffix;
|
#
d4893bed |
|
19-Jan-2018 |
wenzelm <none@none> |
clarified signature;
|
#
16f5c1cb |
|
14-Jan-2018 |
wenzelm <none@none> |
clarified signature;
|
#
c48651e8 |
|
12-Dec-2017 |
wenzelm <none@none> |
scan only one line, for more detailed positions;
|
#
6a7286b7 |
|
01-Apr-2016 |
wenzelm <none@none> |
tuned signature;
|
#
3a4aabc8 |
|
29-Mar-2016 |
wenzelm <none@none> |
clarified reports; tuned signature;
|
#
8f132a85 |
|
20-Jan-2016 |
wenzelm <none@none> |
tuned;
|
#
0c231a3f |
|
06-Nov-2015 |
wenzelm <none@none> |
more formal treatment of control symbols;
|
#
40018461 |
|
20-Oct-2015 |
wenzelm <none@none> |
another antiquotation short form: undecorated cartouche as alias for @{text}; document antiquotation @{text} ignores option "source";
|
#
819078b2 |
|
18-Oct-2015 |
wenzelm <none@none> |
tuned;
|
#
9033287d |
|
18-Oct-2015 |
wenzelm <none@none> |
tuned signature;
|
#
2f33beac |
|
18-Oct-2015 |
wenzelm <none@none> |
tuned signature;
|
#
e7d896ea |
|
18-Oct-2015 |
wenzelm <none@none> |
clarified control antiquotations: decode control symbol to get name; document antiquotations @{emph}, @{bold}; symbol interpretation for \<^emph>; tuned;
|
#
87ebf12f |
|
18-Oct-2015 |
wenzelm <none@none> |
support control symbol antiquotations;
|
#
6a6a64be |
|
16-Oct-2015 |
wenzelm <none@none> |
clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;
|
#
933002eb |
|
15-Oct-2015 |
wenzelm <none@none> |
trim_blanks after read, before eval; clarified Raw_Token: uniform output_text; tuned signature;
|
#
c6c83737 |
|
15-Oct-2015 |
wenzelm <none@none> |
more markup;
|
#
33e17821 |
|
14-Oct-2015 |
wenzelm <none@none> |
clarified;
|
#
c096c0bb |
|
13-Oct-2015 |
wenzelm <none@none> |
added split_lines; tuned signature;
|
#
54c11317 |
|
08-Dec-2014 |
wenzelm <none@none> |
expand ML cartouches to Input.source; tuned signature;
|
#
c460bc8f |
|
29-Nov-2014 |
wenzelm <none@none> |
tuned signature -- prefer Input.source;
|
#
dd6b3a62 |
|
31-Oct-2014 |
wenzelm <none@none> |
discontinued obsolete \<^sync> marker;
|
#
fe7022fa |
|
21-Feb-2014 |
wenzelm <none@none> |
more markup -- complete symbols within antiquotation, notably with broken arguments;
|
#
8540a839 |
|
19-Feb-2014 |
wenzelm <none@none> |
tuned signature;
|
#
50619ce2 |
|
17-Feb-2014 |
wenzelm <none@none> |
more markup;
|
#
7270eb6a |
|
16-Feb-2014 |
wenzelm <none@none> |
support ML antiquotations in Scala; tuned -- more uniform ML vs. Scala;
|
#
6104883c |
|
16-Feb-2014 |
wenzelm <none@none> |
antiquotations within plain text: Scala version in accordance to ML;
|
#
8c1e26f7 |
|
20-Jan-2014 |
wenzelm <none@none> |
tuned signature;
|
#
4e9cdcfc |
|
20-Jan-2014 |
wenzelm <none@none> |
tuned -- more direct err_prefix;
|
#
96d2da5f |
|
19-Jan-2014 |
wenzelm <none@none> |
cartouche within antiquotation;
|
#
435cb06e |
|
23-Aug-2013 |
wenzelm <none@none> |
discontinued unused antiquotation blocks;
|
#
95d64a2f |
|
25-Nov-2012 |
wenzelm <none@none> |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
#
871b69bc |
|
29-Aug-2012 |
wenzelm <none@none> |
renamed Position.str_of to Position.here;
|
#
181e4256 |
|
11-Aug-2012 |
wenzelm <none@none> |
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
|
#
475c25ce |
|
10-Aug-2012 |
wenzelm <none@none> |
proper error prefixes;
|
#
99fd6f8e |
|
28-Nov-2011 |
wenzelm <none@none> |
separate module for concrete Isabelle markup; --HG-- rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala
|
#
b25d2e7e |
|
06-Sep-2011 |
wenzelm <none@none> |
bulk reports for improved message throughput;
|
#
f8ede26a |
|
23-Jul-2011 |
wenzelm <none@none> |
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
|
#
a3e9c2a4 |
|
30-Apr-2011 |
wenzelm <none@none> |
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
|
#
c48a1df7 |
|
30-Apr-2011 |
wenzelm <none@none> |
more uniform variations of scan_string;
|
#
23d2ba43 |
|
17-Sep-2010 |
wenzelm <none@none> |
tuned signature of (Context_)Position.report variants;
|
#
385a78e2 |
|
24-Mar-2009 |
wenzelm <none@none> |
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
|
#
892a7416 |
|
22-Mar-2009 |
wenzelm <none@none> |
export report -- version that actually covers all cases; export check_nesting; simplified read (again);
|
#
5d209727 |
|
22-Mar-2009 |
wenzelm <none@none> |
replaced Antiquote.is_antiq by Antiquote.is_text;
|
#
eef54bbb |
|
20-Mar-2009 |
wenzelm <none@none> |
Antiquote.read: argument for reporting text;
|
#
93baf488 |
|
19-Mar-2009 |
wenzelm <none@none> |
parameterized datatype antiquote and read operation;
|
#
ec038f44 |
|
19-Mar-2009 |
wenzelm <none@none> |
Antiquote.Text: keep full position information;
|
#
066fa40d |
|
19-Mar-2009 |
wenzelm <none@none> |
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early; --HG-- rename : src/Pure/Isar/antiquote.ML => src/Pure/General/antiquote.ML
|