| Mon, 27 Jun 2011 22:20:49 +0200 |
wenzelm |
document antiquotations are managed as theory data, with proper name space and entity markup;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2011 17:51:28 +0200 |
wenzelm |
proper checking of @{ML_antiquotation};
|
file |
diff |
annotate
|
| Tue, 03 May 2011 21:44:05 +0200 |
wenzelm |
use existing \<hyphen>;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Mon, 29 Nov 2010 11:22:40 +0100 |
wenzelm |
added document antiquotation @{file};
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 21:13:10 +0100 |
wenzelm |
more robust treatment of "op IDENT";
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 19:16:27 +0100 |
wenzelm |
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
|
file |
diff |
annotate
|
| Sat, 16 Oct 2010 21:23:34 +0100 |
wenzelm |
more robust treatment of symbolic indentifiers (which may contain colons);
|
file |
diff |
annotate
|
| Fri, 08 Oct 2010 21:49:16 +0100 |
wenzelm |
more on ML antiquotations;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 12:40:20 +0200 |
wenzelm |
proper context for various Thy_Output options, via official configuration options in ML and Isar;
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 23:02:45 +0200 |
wenzelm |
updated manual concerning theory loader;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Sun, 30 May 2010 21:34:19 +0200 |
wenzelm |
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
|
file |
diff |
annotate
|
| Tue, 18 May 2010 10:13:33 +0200 |
wenzelm |
prefer structure Keyword and Parse;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 11:39:08 +0200 |
wenzelm |
proper checking of ML functors (in Poly/ML 5.2 or later);
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 11:31:26 +0200 |
wenzelm |
eliminated escaped symbols;
|
file |
diff |
annotate
|
| Sat, 30 May 2009 11:56:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 21:23:40 +0100 |
wenzelm |
fornal markup for antiquotation options;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 20:34:11 +0100 |
wenzelm |
moved @{ML_functor} and @{ML_text} to Pure;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2009 11:57:48 +0100 |
wenzelm |
adapted ThyOutput.antiquotation;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 21:35:39 +0100 |
wenzelm |
use simplified ThyOutput.antiquotation;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 17:37:18 +0100 |
wenzelm |
adapted to structure Long_Name;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2009 15:01:10 +0100 |
wenzelm |
index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Thu, 26 Feb 2009 20:44:07 +0100 |
wenzelm |
uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
|
file |
diff |
annotate
|
| Sat, 14 Feb 2009 21:34:12 +0100 |
wenzelm |
clean_string/clean_name: proper treatment of \<dash>;
|
file |
diff |
annotate
|
| Wed, 11 Feb 2009 21:39:37 +0100 |
wenzelm |
added "inference" entity;
|
file |
diff |
annotate
|
| Thu, 13 Nov 2008 21:41:04 +0100 |
wenzelm |
ignore ThyOutput.source flag;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2008 15:01:16 +0200 |
wenzelm |
ThyOutput: export some auxiliary operations;
|
file |
diff |
annotate
|
| Mon, 29 Sep 2008 12:31:56 +0200 |
haftmann |
added theory antiquotation
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:38 +0200 |
wenzelm |
simplified ML_Context.eval_in -- expect immutable Proof.context value;
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 14:39:56 +0200 |
wenzelm |
check setting and tool;
|
file |
diff |
annotate
|
| Mon, 15 Sep 2008 16:43:53 +0200 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Mon, 15 Sep 2008 16:43:31 +0200 |
wenzelm |
added formal markup for setting, executable, tool;
|
file |
diff |
annotate
|
| Sat, 09 Aug 2008 22:43:46 +0200 |
wenzelm |
unified Args.T with OuterLex.token, renamed some operations;
|
file |
diff |
annotate
|
| Wed, 25 Jun 2008 17:38:32 +0200 |
wenzelm |
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
|
file |
diff |
annotate
|
| Thu, 15 May 2008 20:02:40 +0200 |
wenzelm |
tuned clean_name (underscore);
|
file |
diff |
annotate
|
| Thu, 15 May 2008 18:03:47 +0200 |
wenzelm |
clean_name: replace "_" by "-";
|
file |
diff |
annotate
|
| Thu, 15 May 2008 17:37:17 +0200 |
wenzelm |
clean_string: cover <;
|
file |
diff |
annotate
|
| Wed, 14 May 2008 20:31:17 +0200 |
wenzelm |
proper checking of various Isar elements;
|
file |
diff |
annotate
|
| Thu, 08 May 2008 22:17:37 +0200 |
wenzelm |
clean_string: map "_" to "\\_" (best used with underscore.sty);
|
file |
diff |
annotate
|
| Wed, 07 May 2008 13:05:13 +0200 |
wenzelm |
output_entity: ignore ThyOutput.source option;
|
file |
diff |
annotate
|
| Tue, 06 May 2008 00:08:52 +0200 |
wenzelm |
element: isakeyword markup;
|
file |
diff |
annotate
|
| Fri, 02 May 2008 22:47:23 +0200 |
wenzelm |
output_entity: added \mbox{} to prevent hyphenation;
|
file |
diff |
annotate
|
| Fri, 02 May 2008 16:36:29 +0200 |
wenzelm |
clean_string: handle { };
|
file |
diff |
annotate
|
| Mon, 28 Apr 2008 14:42:13 +0200 |
wenzelm |
proper command/keyword markup;
|
file |
diff |
annotate
|
| Sat, 26 Apr 2008 13:20:16 +0200 |
wenzelm |
added setup for Isar entities;
|
file |
diff |
annotate
|
| Wed, 23 Apr 2008 15:04:14 +0200 |
wenzelm |
misc cleanup;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 22:22:19 +0200 |
wenzelm |
pretty_term: no revert_skolems here, but auto_fixes (token translations will do the rest);
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 19:12:39 +0100 |
haftmann |
some styling
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 00:02:54 +0100 |
wenzelm |
reorganized signature of ML_Context;
|
file |
diff |
annotate
|
| Mon, 24 Mar 2008 23:34:24 +0100 |
wenzelm |
ML runtime compilation: pass position, tuned signature;
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:35 +0200 |
haftmann |
fixed title
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 16:56:17 +0200 |
wenzelm |
adapted ThyLoad.check_thy;
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 15:33:27 +0200 |
berghofe |
Added named_thms antiquotation.
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:51:51 +0200 |
wenzelm |
renamed ML_exc to ML_exn;
|
file |
diff |
annotate
|
| Sat, 10 Feb 2007 09:26:07 +0100 |
haftmann |
added antiquotation for exceptions
|
file |
diff |
annotate
|