huffman [Thu, 19 Mar 2009 08:13:10 -0700] rev 30598
add lemma det_diagonal; remove wellorder requirement on several lemmas
haftmann [Thu, 19 Mar 2009 14:08:55 +0100] rev 30597
merged
haftmann [Thu, 19 Mar 2009 14:08:41 +0100] rev 30596
tuned some theorem and attribute bindings
wenzelm [Thu, 19 Mar 2009 22:05:00 +0100] rev 30595
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
wenzelm [Thu, 19 Mar 2009 21:05:40 +0100] rev 30594
eval_antiquotes: joint scanning of ML tokens and antiquotations;
wenzelm [Thu, 19 Mar 2009 21:04:53 +0100] rev 30593
added scan_antiq;
more robust scan_ml: plain scanning without cut, regular Symbol_Pos.content instead of Symbol_Pos.implode (which contains spurious Symbol.DEL is used with proper positions);
wenzelm [Thu, 19 Mar 2009 19:49:09 +0100] rev 30592
RAW: provide dummy Isar.main to make tty work gracefully (with ML toplevel);
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!
wenzelm [Thu, 19 Mar 2009 16:56:51 +0100] rev 30590
parameterized datatype antiquote and read operation;
wenzelm [Thu, 19 Mar 2009 15:44:14 +0100] rev 30589
Antiquote.Text: keep full position information;
wenzelm [Thu, 19 Mar 2009 15:22:53 +0100] rev 30588
OuterLex.read_antiq;
wenzelm [Thu, 19 Mar 2009 15:22:53 +0100] rev 30587
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
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;
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.);
wenzelm [Thu, 19 Mar 2009 13:26:19 +0100] rev 30584
Name.of_binding: proper full_name (with checks) before projecting base name;