| Sat, 21 Oct 2023 14:36:47 +0200 |
wenzelm |
more compact ML source;
|
file |
diff |
annotate
|
| Thu, 13 Apr 2023 23:16:18 +0200 |
wenzelm |
compact representation of long name "chunks", with bitmask to suppress elements (i.e. "accesses" in name space terminology);
|
file |
diff |
annotate
|
| Thu, 24 Sep 2020 19:04:47 +0200 |
wenzelm |
proper platform_path for Windows;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2020 15:40:37 +0100 |
wenzelm |
more robust pretty printing of broken YXML, e.g. single "\^E";
|
file |
diff |
annotate
|
| Sat, 30 Mar 2019 20:54:47 +0100 |
wenzelm |
clarified signature: more explicit type Path.binding;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 19:01:20 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 30 Oct 2018 15:45:24 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 26 May 2017 11:51:45 +0200 |
wenzelm |
more correct and complete output of control characters;
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 21:10:07 +0200 |
wenzelm |
careful export of type-dependent functions, without losing their special status;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2016 16:26:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 06 Mar 2016 13:19:19 +0100 |
wenzelm |
clarified ML syntax for strings concerning UTF8;
|
file |
diff |
annotate
|
| Tue, 11 Nov 2014 18:16:25 +0100 |
wenzelm |
more position information, e.g. relevant for errors in generated ML source;
|
file |
diff |
annotate
|
| Mon, 17 Mar 2014 20:22:04 +0100 |
wenzelm |
more robust machine-generated ML sources: constructors for typ and term sometimes occur elsewhere;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 21:10:42 +0100 |
wenzelm |
more uniform Symbol.is_ascii_identifier in ML/Scala;
|
file |
diff |
annotate
|
| Sat, 16 Jul 2011 17:11:49 +0200 |
wenzelm |
added File.fold_pages for streaming of large files;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 11:14:33 +0100 |
wenzelm |
pretty_string: proper handling of negative max_len;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 20:41:33 +0100 |
wenzelm |
tuned ML toplevel pp for type string: observe depth limit;
|
file |
diff |
annotate
|
| Fri, 19 Nov 2010 23:48:07 +0100 |
wenzelm |
total Symbol.explode (cf. 1050315f6ee2);
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 22:42:07 +0200 |
wenzelm |
ML_Syntax.print_char: more readable output of some well-known ASCII controls -- this is relevant for ML toplevel pp;
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 23:20:47 +0200 |
wenzelm |
ML pretty printing of type string according to (quasi-abstract) YXML markup and symbols (including UTF8);
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 11:12:40 +0200 |
wenzelm |
allow Isabelle symbols within low-level ML source;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2009 15:59:42 +0100 |
wenzelm |
added make_binding;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 21:48:40 +0100 |
wenzelm |
added print_properties, print_position (again);
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 23:21:44 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Mon, 24 Mar 2008 17:09:33 +0100 |
wenzelm |
removed unused print_properties, print_position;
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 16:04:32 +0100 |
wenzelm |
added print_properties, print_position;
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:26:17 +0200 |
wenzelm |
ML_Lex.keywords;
|
file |
diff |
annotate
|
| Fri, 14 Sep 2007 17:02:34 +0200 |
wenzelm |
moved ML_XXX.ML files to Pure/ML;
|
file |
diff |
annotate
|