2014-03-10 wenzelm [Mon, 10 Mar 2014 21:58:54 +0100] rev 56036
enabled test in PIDE interaction;
src/FOL/ex/Locale_Test/Locale_Test1.thy

2014-03-10 wenzelm [Mon, 10 Mar 2014 21:40:39 +0100] rev 56035
proper Args.syntax for slightly odd bundle trickery;
do not handle arbitrary exceptions;
more abstract type Args.src;
src/HOL/Tools/Lifting/lifting_setup.ML src/Pure/Isar/args.ML

2014-03-10 wenzelm [Mon, 10 Mar 2014 21:15:29 +0100] rev 56034
some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
src/Pure/PIDE/command.ML src/Pure/PIDE/markup.ML src/Pure/Thy/thy_load.ML src/Pure/Thy/thy_output.ML

2014-03-10 wenzelm [Mon, 10 Mar 2014 20:27:08 +0100] rev 56033
more markup;
src/Pure/Isar/args.ML src/Pure/Isar/attrib.ML src/Pure/PIDE/markup.ML

2014-03-10 wenzelm [Mon, 10 Mar 2014 18:06:23 +0100] rev 56032
clarified Args.check_src: retain name space information for error output;
tuned signature;
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/HOL/Tools/recdef.ML src/HOL/Tools/try0.ML src/Pure/Isar/args.ML src/Pure/Isar/attrib.ML src/Pure/Isar/method.ML src/Pure/ML/ml_context.ML src/Pure/Thy/term_style.ML src/Pure/Thy/thy_output.ML

2014-03-10 wenzelm [Mon, 10 Mar 2014 17:52:30 +0100] rev 56031
tuned;
src/ZF/Tools/ind_cases.ML src/ZF/Tools/inductive_package.ML

2014-03-10 wenzelm [Mon, 10 Mar 2014 17:09:40 +0100] rev 56030
modernized data managed via Name_Space.table;
src/Pure/Thy/term_style.ML

2014-03-10 wenzelm [Mon, 10 Mar 2014 16:30:07 +0100] rev 56029
clarified Args.src: more abstract type, position refers to name only;
prefer self-contained Args.check_src;
src/HOL/Tools/Lifting/lifting_setup.ML src/HOL/Tools/recdef.ML src/Pure/Isar/args.ML src/Pure/Isar/attrib.ML src/Pure/Isar/method.ML src/Pure/Isar/parse_spec.ML src/Pure/ML/ml_context.ML src/Pure/Thy/term_style.ML src/Pure/Thy/thy_output.ML

2014-03-10 wenzelm [Mon, 10 Mar 2014 15:30:29 +0100] rev 56028
tuned signature;
src/Pure/Isar/args.ML src/Pure/Thy/thy_output.ML

2014-03-10 wenzelm [Mon, 10 Mar 2014 15:20:41 +0100] rev 56027
prefer Name_Space.pretty with its builtin markup;
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/HOL/Tools/try0.ML src/Pure/Isar/args.ML src/Pure/Isar/attrib.ML