#
26e81017 |
|
27-Nov-2018 |
wenzelm <none@none> |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups; tuned signature;
|
#
8faaa443 |
|
23-May-2016 |
wenzelm <none@none> |
embedded content may be delimited via cartouches;
|
#
6eb38925 |
|
09-Dec-2015 |
wenzelm <none@none> |
clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
|
#
d6034eb2 |
|
25-Jun-2015 |
wenzelm <none@none> |
tuned signature;
|
#
785df93b |
|
30-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
#
f739ffa6 |
|
25-Mar-2015 |
wenzelm <none@none> |
tuned signature;
|
#
d34da7e7 |
|
10-Mar-2015 |
wenzelm <none@none> |
clarified Token.check_src: intern at most once; Method.parse_internal for Eisbach: intern method names;
|
#
41884eaf |
|
08-Mar-2015 |
wenzelm <none@none> |
cartouche_declaration for Eisbach;
|
#
9bbace2c |
|
29-Nov-2014 |
wenzelm <none@none> |
more abstract type Input.source;
|
#
7f04aae7 |
|
20-Aug-2014 |
wenzelm <none@none> |
support for declaration within token source;
|
#
954f4735 |
|
20-Aug-2014 |
wenzelm <none@none> |
support for nested Token.src within Token.T; tuned signature;
|
#
d65030e5 |
|
19-Aug-2014 |
wenzelm <none@none> |
tuned signature -- moved type src to Token, without aliases;
|
#
459fc7ff |
|
15-Aug-2014 |
wenzelm <none@none> |
more informative Token.Name with history of morphisms; tuned signature;
|
#
308258ec |
|
14-Aug-2014 |
wenzelm <none@none> |
more informative Token.Fact: retain name of dynamic fact (without selection);
|
#
6635fc4f |
|
09-Apr-2014 |
wenzelm <none@none> |
proper Args.name vs. Args.text as documented (in contrast to adhoc union in 75aaee32893d, which had to cope with more limited Args.T);
|
#
e5385d18 |
|
09-Apr-2014 |
wenzelm <none@none> |
allow text cartouches in regular outer syntax categories "text" and "altstring";
|
#
16d1cf5d |
|
31-Mar-2014 |
wenzelm <none@none> |
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
|
#
2ef0938c |
|
17-Mar-2014 |
wenzelm <none@none> |
more markup for improper elements;
|
#
e50a7cf7 |
|
18-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
#
8a9c8afc |
|
18-Mar-2014 |
wenzelm <none@none> |
unused;
|
#
ecc0dc9e |
|
12-Mar-2014 |
wenzelm <none@none> |
more explicit markup for Token.Literal; Markup.quasi_keyword for Parse.$$$ -- it is used within Args.syntax as well; Markup.operator for name of Args.syntax, to override outer keywords like "where"; tuned signature;
|
#
2e37c423 |
|
10-Mar-2014 |
wenzelm <none@none> |
tuned messages -- in accordance to Isabelle/Scala;
|
#
b5f731b0 |
|
10-Mar-2014 |
wenzelm <none@none> |
tuned;
|
#
9d0c860b |
|
10-Mar-2014 |
wenzelm <none@none> |
proper Args.syntax for slightly odd bundle trickery; do not handle arbitrary exceptions; more abstract type Args.src;
|
#
f5e5954d |
|
10-Mar-2014 |
wenzelm <none@none> |
more markup;
|
#
f3fa700b |
|
10-Mar-2014 |
wenzelm <none@none> |
clarified Args.check_src: retain name space information for error output; tuned signature;
|
#
0673c065 |
|
10-Mar-2014 |
wenzelm <none@none> |
clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;
|
#
e0210435 |
|
10-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
#
f1c9f8a2 |
|
10-Mar-2014 |
wenzelm <none@none> |
prefer Name_Space.pretty with its builtin markup;
|
#
3cb75ce2 |
|
09-Mar-2014 |
wenzelm <none@none> |
tuned signature;
|
#
6a3623e0 |
|
08-Mar-2014 |
wenzelm <none@none> |
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
|
#
b7dd9a32 |
|
06-Mar-2014 |
wenzelm <none@none> |
reject internal term names outright, and complete consts instead; more general Name_Space.check_reports; more compact Markup.markup_report;
|
#
36e5d9e2 |
|
06-Mar-2014 |
wenzelm <none@none> |
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
|
#
fe74750f |
|
06-Mar-2014 |
wenzelm <none@none> |
more uniform check_const/read_const;
|
#
8decd8eb |
|
05-Mar-2014 |
wenzelm <none@none> |
tuned signature -- more uniform check_type_name/read_type_name; proper reports for read_type_name (lost in 710bc66f432c);
|
#
b9224853 |
|
05-Mar-2014 |
wenzelm <none@none> |
suppress short abbreviations more uniformly, for outer and quasi-outer syntax; tuned signature;
|
#
57387a0f |
|
05-Mar-2014 |
wenzelm <none@none> |
clarified init_assignable: make double-sure that initial values are reset; more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";
|
#
0e1799d7 |
|
01-Mar-2014 |
wenzelm <none@none> |
clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";
|
#
5da97e94 |
|
25-Feb-2014 |
wenzelm <none@none> |
tuned message -- more markup;
|
#
18efdd72 |
|
24-Feb-2014 |
wenzelm <none@none> |
tuned signature;
|
#
0881c418 |
|
23-Feb-2014 |
wenzelm <none@none> |
tuned message;
|
#
208c8fe5 |
|
26-Jan-2014 |
wenzelm <none@none> |
tuned signature;
|
#
28742b1e |
|
22-Jan-2014 |
wenzelm <none@none> |
tuned signature;
|
#
f15f49f4 |
|
19-Jan-2014 |
wenzelm <none@none> |
cartouche within nested args (attributes, methods, etc.);
|
#
42b5b84f |
|
18-Jan-2014 |
wenzelm <none@none> |
support for nested text cartouches; clarified Symbol.is_symbolic: exclude \<open> and \<close>;
|
#
40fe5f23 |
|
23-Aug-2013 |
wenzelm <none@none> |
tuned signature;
|
#
e3304e81 |
|
20-Aug-2013 |
wenzelm <none@none> |
more careful parsing of nested argument tokens -- avoid Parse.RESET_VALUE on still uninterpreted material;
|
#
554a6a5e |
|
20-Aug-2013 |
wenzelm <none@none> |
proper exhaustive match (cf. e9beabf045ab);
|
#
871b69bc |
|
29-Aug-2012 |
wenzelm <none@none> |
renamed Position.str_of to Position.here;
|
#
a309722d |
|
28-Oct-2011 |
wenzelm <none@none> |
tuned signature -- refined terminology;
|
#
00014899 |
|
21-Aug-2011 |
wenzelm <none@none> |
tuned Parse.group: delayed failure message;
|
#
00fc42cd |
|
23-Apr-2011 |
wenzelm <none@none> |
proper binding/report of defined simprocs; tuned signature;
|
#
87db399e |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
e5f2a357 |
|
30-Oct-2010 |
wenzelm <none@none> |
support for real valued configuration options;
|
#
90cf947c |
|
17-May-2010 |
wenzelm <none@none> |
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time; eliminated slightly odd alias structure T; --HG-- rename : src/Pure/Isar/outer_lex.ML => src/Pure/Isar/token.ML
|
#
6f878766 |
|
15-May-2010 |
wenzelm <none@none> |
refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
|
#
3d057536 |
|
29-Apr-2010 |
wenzelm <none@none> |
ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;
|
#
0ca7694f |
|
13-Mar-2010 |
wenzelm <none@none> |
removed unused Args.maxidx_values and Element.generalize_facts;
|
#
906be7a0 |
|
06-Mar-2010 |
wenzelm <none@none> |
eliminated Args.bang_facts (legacy feature);
|
#
fdac3be8 |
|
27-Feb-2010 |
wenzelm <none@none> |
clarified ProofContext.read_const(_proper)/Args.const(_proper) wrt. strict logical consts;
|
#
dcc68a4d |
|
25-Feb-2010 |
wenzelm <none@none> |
clarified ProofContext.read_type_name/Args.type_name wrt strict logical constructors;
|
#
2a9bf4d9 |
|
06-Feb-2010 |
wenzelm <none@none> |
fixed spelling;
|
#
4254db6e |
|
10-Nov-2009 |
wenzelm <none@none> |
bang_facts: legacy feature;
|
#
2f14c9ed |
|
30-Sep-2009 |
wenzelm <none@none> |
eliminated redundant bindings;
|
#
886198b6 |
|
20-Jul-2009 |
wenzelm <none@none> |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
#
42d1be30 |
|
18-Mar-2009 |
wenzelm <none@none> |
de-camelized Symbol_Pos;
|
#
ef2df2e2 |
|
13-Mar-2009 |
wenzelm <none@none> |
simplified goal_spec: default to first goal;
|
#
da802918 |
|
13-Mar-2009 |
wenzelm <none@none> |
eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
|
#
ee2e7b78 |
|
12-Mar-2009 |
wenzelm <none@none> |
Assumption.all_prems_of, Assumption.all_assms_of;
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
4ad18568 |
|
03-Mar-2009 |
wenzelm <none@none> |
renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify; minor tuning;
|
#
1bd59ac7 |
|
21-Jan-2009 |
wenzelm <none@none> |
removed Ids;
|
#
5823ee39 |
|
21-Jan-2009 |
haftmann <none@none> |
binding is alias for Binding.T
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
740587ab |
|
01-Dec-2008 |
haftmann <none@none> |
new Binding module
|
#
1a4e769c |
|
02-Sep-2008 |
wenzelm <none@none> |
added binding; thm_name/opt_thm_name: Name.binding;
|
#
0f5001b2 |
|
15-Aug-2008 |
wenzelm <none@none> |
Args.name_source(_position) for proper position information;
|
#
d19bcdd3 |
|
09-Aug-2008 |
wenzelm <none@none> |
pass token source to typ/term etc.;
|
#
66d9e8bc |
|
09-Aug-2008 |
wenzelm <none@none> |
unified Args.T with OuterLex.token; moved datatype value/slot and basic operations to outer_lex.ML; removed unused terminator; removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML); removed obsolete thm_sel (cf. attrib.ML); one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);
|
#
247c6726 |
|
04-Aug-2008 |
wenzelm <none@none> |
abstract type Scan.stopper;
|
#
c288dc63 |
|
28-Jun-2008 |
wenzelm <none@none> |
tuned nested args parser; export generic_args1;
|
#
0aec97d2 |
|
28-Jun-2008 |
wenzelm <none@none> |
added thm_name, opt_thm_name;
|
#
6b603959 |
|
26-Jun-2008 |
wenzelm <none@none> |
added context/theory scanner;
|
#
1bc6e514 |
|
16-Jun-2008 |
wenzelm <none@none> |
export eof;
|
#
a46b31e4 |
|
19-Mar-2008 |
wenzelm <none@none> |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
#
6ffa84a1 |
|
28-Jan-2008 |
wenzelm <none@none> |
added ::: / @@@ scanner combinators;
|
#
5f4668da |
|
08-Nov-2007 |
wenzelm <none@none> |
added const_proper;
|
#
656f6e0e |
|
07-Nov-2007 |
wenzelm <none@none> |
Syntax.read_typ;
|
#
ae244bb5 |
|
07-Nov-2007 |
wenzelm <none@none> |
removed obsolete Sign.read_tyname/const (cf. ProofContext);
|
#
d06d005b |
|
08-Oct-2007 |
wenzelm <none@none> |
generic Syntax.pretty/string_of operations;
|
#
ab12469b |
|
01-Sep-2007 |
wenzelm <none@none> |
replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
|
#
c07db288 |
|
13-Aug-2007 |
wenzelm <none@none> |
Lexicon.read_indexname/nat/variable;
|
#
e9eddf4e |
|
27-Jul-2007 |
wenzelm <none@none> |
added terminator, named_attribute;
|
#
72e33780 |
|
10-May-2007 |
wenzelm <none@none> |
bang_facts: warning;
|
#
bd2ca2d6 |
|
13-Apr-2007 |
wenzelm <none@none> |
Morphism.transform/form;
|
#
43b40dae |
|
02-Jan-2007 |
wenzelm <none@none> |
Morphism.fact;
|
#
96056fde |
|
18-Dec-2006 |
haftmann <none@none> |
switched argument order in *.syntax lifters
|
#
241b8ab7 |
|
09-Dec-2006 |
wenzelm <none@none> |
added term_abbrev;
|
#
edbad043 |
|
07-Dec-2006 |
wenzelm <none@none> |
tuned pretty_src output;
|
#
31d1d76f |
|
05-Dec-2006 |
wenzelm <none@none> |
attribute value: morphism;
|
#
38ad6334 |
|
23-Nov-2006 |
wenzelm <none@none> |
renamed Name value to Text, which is *not* a name in terms of morphisms;
|
#
ceb4abb7 |
|
22-Nov-2006 |
wenzelm <none@none> |
replaced map_values by morph_values;
|
#
33e57e7d |
|
14-Oct-2006 |
wenzelm <none@none> |
moved pretty_attribs to attrib.ML;
|
#
fa18480a |
|
21-Sep-2006 |
wenzelm <none@none> |
member (op =);
|
#
66cc9615 |
|
02-Aug-2006 |
wenzelm <none@none> |
normalized Proof.context/method type aliases;
|
#
99d56365 |
|
30-Jul-2006 |
wenzelm <none@none> |
added maxidx_values;
|
#
0ea2b558 |
|
27-Jul-2006 |
wenzelm <none@none> |
moved basic assumption operations from structure ProofContext to Assumption;
|
#
4e5eecff |
|
12-Jul-2006 |
wenzelm <none@none> |
query/bang_colon: separate tokens;
|
#
cf09f0e2 |
|
27-Apr-2006 |
wenzelm <none@none> |
tuned basic list operators (flat, maps, map_filter);
|
#
2487f67c |
|
09-Feb-2006 |
wenzelm <none@none> |
Context.generic is canonical state of parsers; removed obsolete global/local parsers; tuned interfaces;
|
#
acdc5889 |
|
21-Jan-2006 |
wenzelm <none@none> |
simplified type attribute;
|
#
8659c9e7 |
|
10-Jan-2006 |
wenzelm <none@none> |
added generic syntax; mk_attribute: generic;
|
#
794b286c |
|
28-Oct-2005 |
wenzelm <none@none> |
syntax for literal facts;
|
#
0b3955ae |
|
18-Aug-2005 |
wenzelm <none@none> |
removed obsolete Theory.sign_of;
|
#
b3012826 |
|
16-Aug-2005 |
wenzelm <none@none> |
added liberal_name;
|
#
be3f9d9b |
|
08-Jun-2005 |
wenzelm <none@none> |
renamed global/local_typ_raw to global/local_typ_abbrev;
|
#
a921b786 |
|
31-May-2005 |
wenzelm <none@none> |
added symbol scanner;
|
#
3242c88f |
|
17-May-2005 |
wenzelm <none@none> |
Syntax.read_variable;
|
#
fea4cbff |
|
13-Apr-2005 |
wenzelm <none@none> |
*** MESSAGE REFERS TO PREVIOUS VERSION *** support embedded values and static binding -- via implicit assignment to src tokens (cf. assignable/assign/closure); renamed ident/string/keyword to mk_ident/mk_string/mk_keyword; added mk_name, mk_typ, mk_term, mk_fact, mk_attribute; added type value with map_values etc.; removed name_dummy, added general 'maybe' combinator; added global/local_tyname/const; added pretty_src, pretty_attribs; added thm_sel (from attrib.ML);
|
#
0f8c0167 |
|
13-Apr-2005 |
wenzelm <none@none> |
*** empty log message ***
|
#
f527ae4a |
|
09-Mar-2005 |
ballarin <none@none> |
First version of global registration command.
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
704ae032 |
|
29-May-2004 |
wenzelm <none@none> |
do *not* export list/list1 -- commas considered special in arg syntax;
|
#
0362d705 |
|
21-May-2004 |
wenzelm <none@none> |
xxx_typ_raw replace xxx_typ_no_norm forms;
|
#
0a751af7 |
|
19-May-2004 |
chaieb <none@none> |
the function list1 has been exported.
|
#
500be332 |
|
19-Apr-2004 |
kleing <none@none> |
change quote to Library.quote, fixes LaTeX \isarchardoublequote problem.
|
#
dd833639 |
|
14-Apr-2004 |
wenzelm <none@none> |
tuned;
|
#
c25996f5 |
|
29-Aug-2003 |
ballarin <none@none> |
Methods rule_tac etc support static (Isar) contexts.
|
#
5ca65abd |
|
21-Aug-2001 |
wenzelm <none@none> |
tuned error message;
|
#
c8045feb |
|
04-Oct-2000 |
wenzelm <none@none> |
added "bracks";
|
#
211acdc3 |
|
19-Sep-2000 |
wenzelm <none@none> |
added common args keywords;
|
#
2b4b27df |
|
13-Sep-2000 |
wenzelm <none@none> |
Args.addN, Args.delN;
|
#
4820de36 |
|
07-Sep-2000 |
wenzelm <none@none> |
avoid handle_error (better msgs);
|
#
f38bf61b |
|
02-Sep-2000 |
wenzelm <none@none> |
added mode parser;
|
#
ea7b1801 |
|
30-Aug-2000 |
wenzelm <none@none> |
added string_of;
|
#
e82f9fe2 |
|
04-Aug-2000 |
wenzelm <none@none> |
added int;
|
#
af3247a0 |
|
02-Aug-2000 |
wenzelm <none@none> |
typ_no_norm;
|
#
b96789d7 |
|
25-Jun-2000 |
wenzelm <none@none> |
removed obsolete "{}";
|
#
5156bee6 |
|
21-May-2000 |
wenzelm <none@none> |
replaced {{ }} by { };
|
#
b59d437d |
|
05-May-2000 |
wenzelm <none@none> |
GPLed; added colon, parens;
|
#
94114a81 |
|
12-Apr-2000 |
wenzelm <none@none> |
Args.name_dummy;
|
#
fe180fb7 |
|
21-Mar-2000 |
wenzelm <none@none> |
goal_spec: [!];
|
#
39c5e318 |
|
20-Mar-2000 |
wenzelm <none@none> |
goal_spec;
|
#
df6602b3 |
|
22-Feb-2000 |
wenzelm <none@none> |
tuned syntax wrapper;
|
#
987f8b09 |
|
13-Feb-2000 |
wenzelm <none@none> |
attrib: keyword_symid; goal_spec;
|
#
c16cdbc4 |
|
05-Jan-2000 |
wenzelm <none@none> |
removed pats;
|
#
efb9dfda |
|
21-Sep-1999 |
wenzelm <none@none> |
added bang_facts;
|
#
b2e2e0d5 |
|
16-Apr-1999 |
wenzelm <none@none> |
lifted enum; removed list(1); added and_list(1);
|
#
445f6b9a |
|
19-Nov-1998 |
wenzelm <none@none> |
term_pat vs. prop_pat;
|
#
4e03fc9e |
|
17-Nov-1998 |
wenzelm <none@none> |
removed trace;
|
#
2c839f38 |
|
16-Nov-1998 |
wenzelm <none@none> |
several args parsers; include positions; misc tuning;
|
#
3388a142 |
|
09-Nov-1998 |
wenzelm <none@none> |
Concrete argument syntax (for attributes, methods etc.).
|