17 months ago wenzelm [Tue, 12 Dec 2017 17:47:23 +0100] rev 67190
clarified file pattern;
src/Pure/Thy/latex.scala

17 months ago wenzelm [Tue, 12 Dec 2017 17:47:00 +0100] rev 67189
ensure separation of TeX tokens;
src/Pure/Thy/latex.ML

17 months ago wenzelm [Tue, 12 Dec 2017 16:12:48 +0100] rev 67188
simplified positions -- line is also human-readable in generated .tex file;
src/Pure/PIDE/command.ML src/Pure/PIDE/markup.ML src/Pure/Thy/document_antiquotations.ML src/Pure/Thy/latex.ML src/Pure/Thy/latex.scala src/Pure/Thy/thy_output.ML

17 months ago wenzelm [Tue, 12 Dec 2017 13:34:11 +0100] rev 67187
tuned message;
src/Pure/Thy/present.ML src/Pure/Thy/present.scala

17 months ago wenzelm [Tue, 12 Dec 2017 12:35:01 +0100] rev 67186
avoid excessive whitespace between antiquotations and text;
src/Pure/Thy/thy_output.ML

17 months ago wenzelm [Mon, 11 Dec 2017 18:39:24 +0100] rev 67185
updated documentation;
src/Doc/System/Presentation.thy

17 months ago wenzelm [Mon, 11 Dec 2017 17:52:05 +0100] rev 67184
more robust range on preceding comment-line;
no range for blank lines;
avoid recursive output_text/mark_range;
clarified Latex.output_token (no range) vs. Thy_Output.present_token (with range);
src/Pure/PIDE/command.ML src/Pure/Thy/document_antiquotations.ML src/Pure/Thy/latex.ML src/Pure/Thy/latex.scala src/Pure/Thy/thy_output.ML

17 months ago wenzelm [Mon, 11 Dec 2017 17:49:47 +0100] rev 67183
proper file;
src/Pure/Thy/latex.scala

17 months ago wenzelm [Mon, 11 Dec 2017 14:10:41 +0100] rev 67182
clarified file positions;
src/Pure/Thy/latex.scala

17 months ago wenzelm [Mon, 11 Dec 2017 14:10:12 +0100] rev 67181
more operations;
src/Pure/General/path.scala