Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/ML_Bootstrap.thy
author wenzelm
Thu, 07 Apr 2016 16:53:43 +0200
changeset 62902 3c0f53eae166
parent 62893 fca40adc6342
child 62930 51ac6bc389e8
permissions -rw-r--r--
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62887
6b2c60ebd915 clarified ML bootstrap environment;
wenzelm
parents: 62883
diff changeset 
     1
 
(*  Title:      Pure/ML_Bootstrap.thy
62868
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset 
     2
 
    Author:     Makarius
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands;
wenzelm
parents:
diff changeset 
     3
 







62887






6b2c60ebd915
clarified ML bootstrap environment;



wenzelm


parents: 
62883

diff
changeset




     4


ML bootstrap environment -- with access to low-level structures!








62868






61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;



wenzelm


parents: 

diff
changeset




     5


*)













61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;



wenzelm


parents: 

diff
changeset




     6









62887






6b2c60ebd915
clarified ML bootstrap environment;



wenzelm


parents: 
62883

diff
changeset




     7


theory ML_Bootstrap








62880






76e7d9169b54
clarified files;



wenzelm


parents: 
62873

diff
changeset




     8


imports Pure








62868






61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;



wenzelm


parents: 

diff
changeset




     9


begin













61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;



wenzelm


parents: 

diff
changeset




    10









62873






2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;



wenzelm


parents: 
62871

diff
changeset




    11


setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>








62893






fca40adc6342
virtual thread data via context, for proper support of Context.>> etc;



wenzelm


parents: 
62887

diff
changeset




    12


SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close>








62902






3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';



wenzelm


parents: 
62893

diff
changeset




    13


setup \<open>Config.put_global ML_Env.SML_environment true\<close>








62868






61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;



wenzelm


parents: 

diff
changeset




    14














61a691db1c4d
support for ML project ROOT file, with imitation of ML "use" commands;



wenzelm


parents: 

diff
changeset




    15


end















isabelle