| Sun, 12 May 2013 20:25:45 +0200 |
wenzelm |
some system options as context-sensitive config options;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2012 20:38:02 +0200 |
wenzelm |
clarified output token markup (see also bc22daeed49e);
|
file |
diff |
annotate
|
| Wed, 03 Oct 2012 16:59:58 +0200 |
wenzelm |
more explicit show_type_constraint, show_sort_constraint;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 16:17:46 +0200 |
wenzelm |
turn constraints into Isabelle_Markup.typing, depending on show_markup options;
|
file |
diff |
annotate
|
| Sat, 29 Sep 2012 13:43:23 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 02 May 2012 16:56:25 +0200 |
wenzelm |
avoid interference of markup for literal tokens, which may contain slightly odd \<^bsub> \<^esub> counted as pseudo-markup (especially relevant for HTML output, e.g. of thm power3_eq_cube);
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 23:47:05 +0200 |
wenzelm |
provide structure Syntax early (before structure Type), back-patch check/uncheck later;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 21:11:29 +0200 |
wenzelm |
discontinued Syntax.max_pri, which is not really a symbolic parameter;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 15:48:14 +0200 |
wenzelm |
discontinued special status of structure Printer;
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 15:02:11 +0200 |
wenzelm |
discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext);
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
| Thu, 07 Apr 2011 17:52:44 +0200 |
wenzelm |
simplified printer context: uniform externing and static token translations;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 21:55:41 +0200 |
wenzelm |
moved type syntax translations to syn_trans.ML;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 17:00:40 +0200 |
wenzelm |
more abstract print translation;
|
file |
diff |
annotate
|
| Wed, 06 Apr 2011 12:58:13 +0200 |
wenzelm |
moved unparse material to syntax_phases.ML;
|
file |
diff |
annotate
|
| Tue, 22 Mar 2011 13:32:20 +0100 |
wenzelm |
support for encoded positions (for id_position, longid_position) as pseudo type-constraints -- still inactive;
|
file |
diff |
annotate
|
| Sat, 04 Dec 2010 14:57:04 +0100 |
wenzelm |
added Syntax.pretty_priority;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2010 21:33:19 +0200 |
wenzelm |
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 23:16:21 +0200 |
wenzelm |
turned show_brackets into proper configuration option;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 21:41:24 +0200 |
wenzelm |
turned show_sorts/show_types into proper configuration options;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 23:54:48 +0200 |
wenzelm |
turned eta_contract into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 22:57:21 +0200 |
wenzelm |
turned show_structs into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 17:43:44 +0200 |
wenzelm |
turned show_all_types into proper configuration option;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 16:36:33 +0200 |
wenzelm |
treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 16:09:12 +0200 |
wenzelm |
more explicit Config.declare vs. Config.declare_global;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 15:54:03 +0200 |
wenzelm |
turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 00:48:07 +0200 |
wenzelm |
turned show_question_marks into proper configuration option;
|
file |
diff |
annotate
|
| Tue, 20 Jul 2010 14:44:33 +0200 |
wenzelm |
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
|
file |
diff |
annotate
|
| Mon, 31 May 2010 21:06:57 +0200 |
wenzelm |
modernized some structure names, keeping a few legacy aliases;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 12:03:47 +0100 |
wenzelm |
mark_atoms: more precise treatment of SynExt.standard_token_markers vs. syntax consts;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2010 00:28:22 +0100 |
wenzelm |
authentic syntax for classes and type constructors;
|
file |
diff |
annotate
|
| Sun, 21 Feb 2010 22:35:02 +0100 |
wenzelm |
slightly more abstract syntax mark/unmark operations;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
file |
diff |
annotate
|
| Tue, 29 Sep 2009 11:49:22 +0200 |
wenzelm |
explicit indication of Unsynchronized.ref;
|
file |
diff |
annotate
|
| Mon, 19 Jan 2009 20:05:41 +0100 |
wenzelm |
removed Ids;
|
file |
diff |
annotate
|
| Thu, 17 Apr 2008 16:30:52 +0200 |
wenzelm |
token translations: context dependent, result Pretty.T;
|
file |
diff |
annotate
|
| Sun, 11 Nov 2007 14:00:12 +0100 |
wenzelm |
replaced extend_prtabs by update_prtabs (absorb duplicates);
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 23:04:02 +0100 |
wenzelm |
remove_prtabs: tuned, avoid excessive garbage;
|
file |
diff |
annotate
|
| Mon, 17 Sep 2007 16:36:41 +0200 |
wenzelm |
avoid direct access to print_mode;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 19:45:44 +0200 |
wenzelm |
eliminated transform_failure (to avoid critical section for main transactions);
|
file |
diff |
annotate
|
| Mon, 09 Jul 2007 11:44:20 +0200 |
wenzelm |
type output = string indicates raw system output;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 12:16:18 +0200 |
wenzelm |
pretty: markup for syntax/name of authentic consts;
|
file |
diff |
annotate
|
| Sat, 07 Jul 2007 00:14:56 +0200 |
wenzelm |
simplified pretty token metric: type int;
|
file |
diff |
annotate
|
| Mon, 11 Dec 2006 21:39:26 +0100 |
wenzelm |
advanced translation functions: Proof.context;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 15:30:48 +0100 |
wenzelm |
support printing of idtdummy;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:33 +0200 |
wenzelm |
pretty: late externing of consts (support authentic syntax);
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:34:55 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
file |
diff |
annotate
|
| Wed, 08 Feb 2006 14:39:00 +0100 |
haftmann |
introduced gen_distinct in place of distinct
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:57 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2006 00:39:40 +0100 |
wenzelm |
advanced translations: Context.generic;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 16:26:54 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:49 +0200 |
wenzelm |
replaced TRANSLATION_FAIL by EXCEPTION;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 18:48:50 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 09:37:12 +0200 |
haftmann |
introduced AList.*
|
file |
diff |
annotate
|
| Mon, 29 Aug 2005 16:18:04 +0200 |
wenzelm |
use AList operations;
|
file |
diff |
annotate
|
| Wed, 29 Jun 2005 15:13:41 +0200 |
wenzelm |
proper treatment of advanced trfuns: pass thy argument;
|
file |
diff |
annotate
|
| Tue, 17 May 2005 10:19:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 23 Apr 2005 19:51:35 +0200 |
wenzelm |
SynExt.standard_token_markers
|
file |
diff |
annotate
|
| Sun, 17 Apr 2005 19:39:11 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2005 18:58:18 +0200 |
wenzelm |
tuned extend_prtabs;
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sun, 20 Jun 2004 09:27:17 +0200 |
wenzelm |
tuned pp;
|
file |
diff |
annotate
|
| Sat, 29 May 2004 15:07:29 +0200 |
wenzelm |
added pp_show_brackets; support unbreakable blocks;
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:22:10 +0200 |
wenzelm |
string_of_vname moved to term.ML;
|
file |
diff |
annotate
|
| Sat, 01 May 2004 22:09:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 29 Aug 2003 18:39:47 +0200 |
skalberg |
Added show_all_types flag, such that all type information in the term
|
file |
diff |
annotate
|
| Wed, 16 Jan 2002 23:19:34 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Sat, 24 Nov 2001 17:01:00 +0100 |
wenzelm |
Symtab.merge_multi';
|
file |
diff |
annotate
|
| Tue, 20 Nov 2001 20:57:46 +0100 |
wenzelm |
prefer later trfuns;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2001 00:35:30 +0200 |
wenzelm |
be more careful about token class markers;
|
file |
diff |
annotate
|
| Thu, 07 Sep 2000 22:37:59 +0200 |
wenzelm |
internalize error "insufficient syntax for prefix application";
|
file |
diff |
annotate
|
| Wed, 15 Mar 2000 18:19:06 +0100 |
wenzelm |
use Pretty.str / Pretty.raw_str;
|
file |
diff |
annotate
|
| Fri, 04 Jun 1999 19:51:04 +0200 |
wenzelm |
print "..." variable;
|
file |
diff |
annotate
|
| Tue, 09 Mar 1999 12:11:29 +0100 |
wenzelm |
token translation: real;
|
file |
diff |
annotate
|
| Fri, 12 Feb 1999 13:56:21 +0100 |
wenzelm |
tuned pretty format lookup;
|
file |
diff |
annotate
|
| Thu, 11 Feb 1999 21:17:10 +0100 |
wenzelm |
proper handling of print_mode wrt. Pretty.sym;
|
file |
diff |
annotate
|
| Fri, 29 Jan 1999 17:10:26 +0100 |
oheimb |
moved print_mode to ROOT.ML
|
file |
diff |
annotate
|
| Tue, 20 Oct 1998 16:32:20 +0200 |
wenzelm |
no open;
|
file |
diff |
annotate
|
| Mon, 09 Mar 1998 16:11:13 +0100 |
wenzelm |
Symbol.output;
|
file |
diff |
annotate
|
| Sun, 28 Dec 1997 14:56:44 +0100 |
wenzelm |
renamed Symtab.null to Symtab.empty;
|
file |
diff |
annotate
|
| Wed, 05 Nov 1997 11:42:19 +0100 |
wenzelm |
print translation: added show_sorts argument;
|
file |
diff |
annotate
|
| Thu, 09 Oct 1997 14:56:52 +0200 |
wenzelm |
changed preference order of prtab entries;
|
file |
diff |
annotate
|
| Mon, 06 Oct 1997 18:22:22 +0200 |
wenzelm |
added sort_to_ast;
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 19:07:54 +0200 |
wenzelm |
fixed diagnostic output of print modes;
|
file |
diff |
annotate
|
| Mon, 31 Mar 1997 14:42:13 +0200 |
wenzelm |
simple_ast_of: fixed handling of loose Bounds;
|
file |
diff |
annotate
|
| Fri, 28 Feb 1997 16:47:56 +0100 |
wenzelm |
split ast_of_term(T);
|
file |
diff |
annotate
|
| Mon, 13 Jan 1997 18:24:40 +0100 |
wenzelm |
improved error msg;
|
file |
diff |
annotate
|
| Fri, 13 Dec 1996 17:37:11 +0100 |
wenzelm |
removed chartrans_of;
|
file |
diff |
annotate
|
| Tue, 10 Dec 1996 13:00:52 +0100 |
wenzelm |
added chartrans_of;
|
file |
diff |
annotate
|
| Tue, 26 Nov 1996 16:26:06 +0100 |
paulson |
Eta-expansion of a function definition, for value polymorphism
|
file |
diff |
annotate
|
| Tue, 19 Nov 1996 13:21:28 +0100 |
wenzelm |
removed old commented out text;
|
file |
diff |
annotate
|
| Mon, 18 Nov 1996 17:29:49 +0100 |
wenzelm |
added print_mode: string list ref (order of printer tables);
|
file |
diff |
annotate
|
| Fri, 16 Feb 1996 16:56:04 +0100 |
paulson |
Elimination of fully-functorial style.
|
file |
diff |
annotate
|
| Wed, 03 May 1995 13:40:19 +0200 |
lcp |
Now show_sorts:=true causes printing of types
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 11:48:05 +0100 |
clasohm |
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
|
file |
diff |
annotate
|
| Mon, 26 Sep 1994 17:35:23 +0100 |
wenzelm |
added flag show_no_free_types: bool ref;
|
file |
diff |
annotate
|
| Fri, 19 Aug 1994 15:37:05 +0200 |
wenzelm |
various minor internal changes;
|
file |
diff |
annotate
|
| Wed, 03 Aug 1994 09:45:42 +0200 |
nipkow |
improved show_brackets again - Trueprop does not create () any more.
|
file |
diff |
annotate
|
| Tue, 02 Aug 1994 20:08:57 +0200 |
nipkow |
minimized () in forced printing of barckets (show_brackets)
|
file |
diff |
annotate
|
| Tue, 02 Aug 1994 09:07:10 +0200 |
nipkow |
added flag show_brackets for printinmg fully bracketed terms.
|
file |
diff |
annotate
|
| Thu, 19 May 1994 16:13:51 +0200 |
wenzelm |
replaced fix_aprop by prop_tr';
|
file |
diff |
annotate
|
| Thu, 03 Feb 1994 13:59:00 +0100 |
wenzelm |
minor internal changes;
|
file |
diff |
annotate
|
| Wed, 19 Jan 1994 14:21:26 +0100 |
wenzelm |
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
|
file |
diff |
annotate
|
| Thu, 21 Oct 1993 14:40:06 +0100 |
lcp |
Pure/Syntax/printer/is_prop: now calls fastype_of1
|
file |
diff |
annotate
|
| Mon, 11 Oct 1993 12:30:06 +0100 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 08 Oct 1993 13:55:04 +0100 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 04 Oct 1993 15:30:49 +0100 |
wenzelm |
lots of internal cleaning and tuning;
|
file |
diff |
annotate
|
| Thu, 16 Sep 1993 12:20:38 +0200 |
clasohm |
Initial revision
|
file |
diff |
annotate
|