src/Pure/Thy/thy_output.ML
2 months ago ago clarified signature;
2 months ago ago clarified Toplevel.state: more explicit types;
2 months ago ago clarified modules;
4 months ago ago support for isabelle update -u control_cartouches;
10 months ago ago clarified syntax;
10 months ago ago simplified: allow only command names, with dummy for default;
10 months ago ago clarified: more uniform keyword_tags;
10 months ago ago tuned;
10 months ago ago more flexible document_tags;
10 months ago ago prefer explicit options;
10 months ago ago clarified default tag;
11 months ago ago clarified signature;
12 months ago ago tuned;
12 months ago ago tuned signature (see Command.eval_state);
12 months ago ago more explicit type Thy_Output.segment;
15 months ago ago clarified signature;
15 months ago ago more uniform treatment of formal comments within document source;
15 months ago ago just one check of formal comments;
15 months ago ago avoid proliferation of language_document reports;
15 months ago ago clarified overall range: include delimiters;
15 months ago ago clarified take/drop/chop prefix/suffix;
15 months ago ago verbatim output consists of plain lines;
15 months ago ago more markup: disable spell-checker for raw latex;
15 months ago ago clarified signature: items with \isasep are special;
16 months ago ago disable "display" style in marginal (line) comment;
16 months ago ago more uniform output of source / text / theory_text, with handling of formal comments etc.;
16 months ago ago tuned;
16 months ago ago clarified access to antiquotation options;
16 months ago ago tuned signature;
16 months ago ago discontinued old form of marginal comments;
16 months ago ago more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
16 months ago ago allow LaTeX source as formal comment;
16 months ago ago clarified modules: uniform notion of formal comments;
16 months ago ago allow TeX comment % in formal comment body, but avoid extra space (cf. d7c6054b2ab1);
16 months ago ago added \<^cancel> operator for unused text;
16 months ago ago more accurate position for enclosing cartouche;
16 months ago ago clarified markup: more like outer syntax side-comment;
16 months ago ago clarified modules;
16 months ago ago theory Pure is default presentation context;
16 months ago ago tuned;
16 months ago ago check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
16 months ago ago tuned;
16 months ago ago clarified output (see also 909dcdec2122, 34d1913f0b20);
16 months ago ago tuned;
16 months ago ago tuned;
16 months ago ago more uniform output: formal comments within {* ... *};
16 months ago ago tuned;
16 months ago ago clarified output: avoid extra space;
16 months ago ago output token content with formal comments and antiquotations;
16 months ago ago clarified signature;
16 months ago ago clarified modules;
17 months ago ago positions as postlude: avoid intrusion of odd %-forms into main tex source;
17 months ago ago option document_positions;
17 months ago ago simplified positions -- line is also human-readable in generated .tex file;
17 months ago ago avoid excessive whitespace between antiquotations and text;
17 months ago ago more robust range on preceding comment-line;
17 months ago ago more explicit latex errors;
17 months ago ago prefer control symbol antiquotations;
17 months ago ago system option for default command tags;
23 months ago ago tuned signature;