isabelle: File revisions

src/Pure/Syntax/syntax.ML

2008-12-05	haftmann	2008-12-05	removed Table.extend, NameSpace.extend_table	file \| diff \| annotate
2008-11-29	nipkow	2008-11-29	New lexical item "float".	file \| diff \| annotate
2008-11-18	wenzelm	2008-11-18	tuned;	file \| diff \| annotate
2008-09-29	wenzelm	2008-09-29	report_token/parse_token: back to context-less version;	file \| diff \| annotate
2008-09-29	wenzelm	2008-09-29	ContextPosition.report; parse_token/report_token: explicit context;	file \| diff \| annotate
2008-09-26	wenzelm	2008-09-26	eliminated polymorphic equality;	file \| diff \| annotate
2008-08-15	wenzelm	2008-08-15	read_asts: Lexicon.report_token, filter Lexicon.is_proper; report tokens;	file \| diff \| annotate
2008-08-10	wenzelm	2008-08-10	added parse_token (from proof_context.ML);	file \| diff \| annotate
2008-08-09	wenzelm	2008-08-09	read_asts: report literal tokens;	file \| diff \| annotate
2008-08-09	wenzelm	2008-08-09	read_token: more robust handling of empty text;	file \| diff \| annotate
2008-08-07	wenzelm	2008-08-07	added read_token -- with optional YXML encoding of position; tuned parse operations: print position instead of echoing input (now encoded!); do not export obsolete read operation;	file \| diff \| annotate
2008-08-07	wenzelm	2008-08-07	adapted Scan.extend_lexicon/merge_lexicons;	file \| diff \| annotate
2008-06-18	wenzelm	2008-06-18	TypeExt.type_constraint;	file \| diff \| annotate
2008-06-13	wenzelm	2008-06-13	map_const: soft version, no failure here;	file \| diff \| annotate
2008-05-18	wenzelm	2008-05-18	moved global pretty/string_of functions from Sign to Syntax; reordered signature;	file \| diff \| annotate
2008-04-17	wenzelm	2008-04-17	token translations: context dependent, result Pretty.T; string_of_term/prop: Variable.auto_fixes;	file \| diff \| annotate
2008-04-16	wenzelm	2008-04-16	tuned;	file \| diff \| annotate
2008-04-16	haftmann	2008-04-16	educated guess for infix syntax	file \| diff \| annotate
2008-01-27	wenzelm	2008-01-27	added ambiguity_limit (restricts parse trees / terms printed in messages); tuned;	file \| diff \| annotate
2007-11-27	wenzelm	2007-11-27	standard_parse_term: check ambiguous results without changing the result yet;	file \| diff \| annotate
2007-11-11	wenzelm	2007-11-11	syntax operations: turned extend'' into update'' (absorb duplicates); tuned signature;	file \| diff \| annotate
2007-11-10	wenzelm	2007-11-10	added update_const_gram (avoids duplicates); tuned;	file \| diff \| annotate
2007-10-20	wenzelm	2007-10-20	moved internalM to PrintMode.internal; PrintMode.input;	file \| diff \| annotate
2007-10-16	wenzelm	2007-10-16	Syntax.(un)check: explicit result option;	file \| diff \| annotate
2007-10-15	wenzelm	2007-10-15	unparse_arity: unparse type constructor as well;	file \| diff \| annotate
2007-10-11	wenzelm	2007-10-11	renamed Syntax.XXX_mode to Syntax.mode_XXX; moved ProofContext.pp to Syntax.pp;	file \| diff \| annotate
2007-10-09	wenzelm	2007-10-09	generic Syntax.pretty/string_of operations; added uncheck/unparse_classrel/arity (from sign.ML); tuned;	file \| diff \| annotate
2007-09-29	wenzelm	2007-09-29	added unparse interfaces (still unused); add_typ/term_check: added stage and name argument; added print_checks;	file \| diff \| annotate
2007-09-25	wenzelm	2007-09-25	removed redundant global_parse operations; renamed global_XXX to XXX_global;	file \| diff \| annotate
2007-09-23	wenzelm	2007-09-23	TypeInfer.constrain: canonical argument order;	file \| diff \| annotate
2007-09-17	wenzelm	2007-09-17	added print_mode_value (CRITICAL);	file \| diff \| annotate
2007-09-01	wenzelm	2007-09-01	added singleton check_typ/term/prop;	file \| diff \| annotate
2007-08-30	wenzelm	2007-08-30	turned type_check into separate typ/term_check; tuned sifnature;	file \| diff \| annotate
2007-08-20	wenzelm	2007-08-20	standard_parse_term: added pp/check argument, include disambig here (from sign.ML);	file \| diff \| annotate
2007-08-20	wenzelm	2007-08-20	type_check: tuned singleton funs case;	file \| diff \| annotate
2007-08-14	wenzelm	2007-08-14	renamed standard_read_XXX to standard_parse_XXX; added global_read/parse_XXX;	file \| diff \| annotate
2007-08-14	wenzelm	2007-08-14	added generic wrapper for parse/read functions; renamed read_term to standard_read_term etc.;	file \| diff \| annotate
2007-08-13	wenzelm	2007-08-13	moved appl syntax to PureThy; structure Lexicon: not hidden;	file \| diff \| annotate
2007-07-23	wenzelm	2007-07-23	hide internal structures (again);	file \| diff \| annotate
2007-07-09	wenzelm	2007-07-09	type output = string indicates raw system output;	file \| diff \| annotate
2007-07-08	wenzelm	2007-07-08	replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;	file \| diff \| annotate
2007-07-07	wenzelm	2007-07-07	pretty_sort/typ/term: markup;	file \| diff \| annotate
2007-07-07	wenzelm	2007-07-07	simplified pretty token metric: type int;	file \| diff \| annotate
2007-04-21	wenzelm	2007-04-21	TypeExt.decode_term;	file \| diff \| annotate
2007-04-15	wenzelm	2007-04-15	added read_term; adapted decoding of types/sorts;	file \| diff \| annotate
2007-04-03	wenzelm	2007-04-03	avoid clash with Alice keywords;	file \| diff \| annotate
2007-01-19	wenzelm	2007-01-19	tuned Scan.extend_lexicon;	file \| diff \| annotate
2006-12-30	wenzelm	2006-12-30	removed conditional combinator;	file \| diff \| annotate
2006-12-13	wenzelm	2006-12-13	tuned signature;	file \| diff \| annotate
2006-12-11	wenzelm	2006-12-11	advanced translation functions: Proof.context;	file \| diff \| annotate
2006-12-09	wenzelm	2006-12-09	added internal_mode;	file \| diff \| annotate
2006-12-07	wenzelm	2006-12-07	added input_mode;	file \| diff \| annotate
2006-11-26	wenzelm	2006-11-26	extend_trtab: allow identical trfuns to be overwritten;	file \| diff \| annotate
2006-09-29	wenzelm	2006-09-29	Syntax.mode;	file \| diff \| annotate
2006-09-21	wenzelm	2006-09-21	member (op =);	file \| diff \| annotate
2006-05-02	wenzelm	2006-05-02	extend/remove_syntax: observe inout flag for translations, too;	file \| diff \| annotate
2006-04-27	wenzelm	2006-04-27	tuned basic list operators (flat, maps, map_filter);	file \| diff \| annotate
2006-04-08	wenzelm	2006-04-08	pretty_term: late externing of consts (support authentic syntax);	file \| diff \| annotate
2006-03-21	wenzelm	2006-03-21	subtract (op =);	file \| diff \| annotate
2006-03-14	wenzelm	2006-03-14	added remove_trrules(_i); tuned;	file \| diff \| annotate

isabelle

RSS Atom