src/Pure/ROOT.ML
changeset 23825 e0372eba47b7
parent 23696 ff97a943681e
child 23986 c656557b73d5
     1.1 --- a/src/Pure/ROOT.ML	Tue Jul 17 13:19:19 2007 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Tue Jul 17 13:19:20 2007 +0200
     1.3 @@ -7,17 +7,15 @@
     1.4  val banner = "Pure Isabelle";
     1.5  val version = "Isabelle repository version";    (*filled in automatically!*)
     1.6  
     1.7 +(*if true then some tools will OMIT some proofs*)
     1.8 +val quick_and_dirty = ref false;
     1.9 +
    1.10  print_depth 10;
    1.11  
    1.12  (*basic tools*)
    1.13  use "General/basics.ML";
    1.14  use "library.ML";
    1.15  
    1.16 -(*generic non-sense*)
    1.17 -val quick_and_dirty = ref false;
    1.18 -val print_mode = ref ([]: string list);
    1.19 -fun print_mode_active s = member (op =) (! print_mode) s;
    1.20 -
    1.21  cd "General"; use "ROOT.ML"; cd "..";
    1.22  
    1.23  (*fundamental structures*)
    1.24 @@ -42,15 +40,6 @@
    1.25  use "Syntax/mixfix.ML";
    1.26  use "Syntax/printer.ML";
    1.27  use "Syntax/syntax.ML";
    1.28 -structure Hidden = struct end;
    1.29 -structure Lexicon = Hidden;
    1.30 -structure Ast = Hidden;
    1.31 -structure SynExt = Hidden;
    1.32 -structure Parser = Hidden;
    1.33 -structure TypeExt = Hidden;
    1.34 -structure SynTrans = Hidden;
    1.35 -structure Mixfix = Hidden;
    1.36 -structure Printer = Hidden;
    1.37  
    1.38  use "General/ml_syntax.ML";
    1.39  
    1.40 @@ -99,19 +88,4 @@
    1.41  (*configuration for Proof General*)
    1.42  cd "ProofGeneral"; use "ROOT.ML"; cd "..";
    1.43  
    1.44 -use_thy "Pure";
    1.45 -structure Pure = struct val thy = theory "Pure" end;
    1.46 -
    1.47 -Context.add_setup
    1.48 - (Sign.del_modesyntax Syntax.default_mode Syntax.appl_syntax #>
    1.49 -  Sign.add_syntax Syntax.applC_syntax);
    1.50 -use_thy "CPure";
    1.51 -structure CPure = struct val thy = theory "CPure" end;
    1.52 -
    1.53 -(*final ML setup*)
    1.54 -use "install_pp.ML";
    1.55 -val use = ThyInfo.use;
    1.56 -val cd = File.cd o Path.explode;
    1.57 -ml_prompts "ML> " "ML# ";
    1.58 -
    1.59 -proofs := 0;
    1.60 +use "pure_setup.ML";