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

2014-03-10 wenzelm [Mon, 10 Mar 2014 15:04:01 +0100] rev 56026
tuned signature -- prefer Name_Space.get with its builtin error;
src/HOL/Tools/Lifting/lifting_setup.ML src/Pure/Isar/attrib.ML src/Pure/Isar/bundle.ML src/Pure/Isar/method.ML src/Pure/Isar/specification.ML src/Pure/sign.ML

2014-03-10 wenzelm [Mon, 10 Mar 2014 13:55:03 +0100] rev 56025
abstract type Name_Space.table;
clarified pretty_locale_deps: sort strings;
clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
src/HOL/Mutabelle/mutabelle.ML src/HOL/Tools/inductive.ML src/Pure/General/name_space.ML src/Pure/Isar/attrib.ML src/Pure/Isar/bundle.ML src/Pure/Isar/locale.ML src/Pure/Isar/method.ML src/Pure/Isar/proof_context.ML src/Pure/Tools/find_consts.ML src/Pure/consts.ML src/Pure/display.ML src/Pure/facts.ML src/Pure/sign.ML src/Pure/term_sharing.ML src/Pure/theory.ML src/Pure/thm.ML src/Pure/type.ML src/Pure/variable.ML src/Tools/Code/code_thingol.ML