[isabelle-dev] isabelle build

[Makarius]

On Mon, 6 Aug 2012, Christian Urban wrote:

> 2) Transferring the IsaMakefile and ROOT.ML file of the Isabelle
>   Cookbook to the new ROOT (see below) has thrown up the following
>   problem:
>
>     ...
>     *** Theory loader: failed to load "Simple_Inductive_Package" (unresolved "Base")
>     *** Inconsistent declaration of outer syntax keyword "ML"
>     *** At command "theory" (line 1 of "/Users/cu/isabelle-cookbook/ProgTutorial/Base.thy")
>
>  The Base.thy (see below) file redefines several "core" Isabelle
>  keywords, which was OK with the old ways (if one knew what one is
>  doing). Is this now seriously prevented?

There used to be a time when the main consts of the HOL axiomatization 
were open to be re-defined in user space, but there was no check for that 
because one would expect that users know what they are better not doing.

Anyway, overwriting Isabelle/Isar commands still happens to work, even 
after the Pure collection has acquired a more formal status than before 
(see changes leading up to a5144c4c26a2).

Here is an example:

ML {*
   val _ =
   Outer_Syntax.command (("ML", Keyword.thy_decl), Position.none)
     "ML text within theory or local theory"
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.generic_theory
         (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
           Local_Theory.propagate_ml_env)));
*}

ML {* Keyword.command_keyword "ML" *}

This changes the tags of the command, which was the main purpose in the 
cookbook, IIRC.

Note that there are no 'keywords' declarations in the header, because they 
are already in Pure.thy.


 	Makarius