Thu, 19 Mar 2009 18:20:27 +0100 added tokenize;
wenzelm [Thu, 19 Mar 2009 18:20:27 +0100] rev 30591
added tokenize; internal scan_str: ensure Symbol.is_regular, otherwise it might swallow the stopper and crash!
Thu, 19 Mar 2009 16:56:51 +0100 parameterized datatype antiquote and read operation;
wenzelm [Thu, 19 Mar 2009 16:56:51 +0100] rev 30590
parameterized datatype antiquote and read operation;
Thu, 19 Mar 2009 15:44:14 +0100 Antiquote.Text: keep full position information;
wenzelm [Thu, 19 Mar 2009 15:44:14 +0100] rev 30589
Antiquote.Text: keep full position information;
Thu, 19 Mar 2009 15:22:53 +0100 OuterLex.read_antiq;
wenzelm [Thu, 19 Mar 2009 15:22:53 +0100] rev 30588
OuterLex.read_antiq;
Thu, 19 Mar 2009 15:22:53 +0100 moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm [Thu, 19 Mar 2009 15:22:53 +0100] rev 30587
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
Thu, 19 Mar 2009 15:22:53 +0100 moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML;
wenzelm [Thu, 19 Mar 2009 15:22:53 +0100] rev 30586
moved basic change_prompt, scan_string, scan_alt_string, scan_quoted to symbol_pos.ML; scan_comment: recovered change_prompt; moved read_antiq to outer_lex.ML;
Thu, 19 Mar 2009 13:28:55 +0100 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
wenzelm [Thu, 19 Mar 2009 13:28:55 +0100] rev 30585
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
Thu, 19 Mar 2009 13:26:19 +0100 Name.of_binding: proper full_name (with checks) before projecting base name;
wenzelm [Thu, 19 Mar 2009 13:26:19 +0100] rev 30584
Name.of_binding: proper full_name (with checks) before projecting base name;
Thu, 19 Mar 2009 11:51:49 +0100 merged
wenzelm [Thu, 19 Mar 2009 11:51:49 +0100] rev 30583
merged
Thu, 19 Mar 2009 01:29:19 -0700 imported patch euclidean
huffman [Thu, 19 Mar 2009 01:29:19 -0700] rev 30582
imported patch euclidean
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip