tuned;
authorwenzelm
Mon Aug 27 14:31:52 2018 +0200 (13 months ago)
changeset 688156296915dee6e
parent 68814 6a0b1357bded
child 68816 5a53724fe247
tuned;
src/Pure/ML/ml_name_space.ML
     1.1 --- a/src/Pure/ML/ml_name_space.ML	Sun Aug 26 17:48:35 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_name_space.ML	Mon Aug 27 14:31:52 2018 +0200
     1.3 @@ -12,8 +12,8 @@
     1.4    val forget_val: string -> unit
     1.5    val forget_type: string -> unit
     1.6    val forget_structure: string -> unit
     1.7 +  val hidden_structures: string list
     1.8    val bootstrap_values: string list
     1.9 -  val hidden_structures: string list
    1.10    val bootstrap_structures: string list
    1.11    val bootstrap_signatures: string list
    1.12    val sml_val: (string * PolyML.NameSpace.Values.value) list
    1.13 @@ -64,13 +64,14 @@
    1.14  val forget_type = PolyML.Compiler.forgetType;
    1.15  val forget_structure = PolyML.Compiler.forgetStructure;
    1.16  
    1.17 +val hidden_structures = ["CInterface", "Foreign", "RunCall", "Signal"];
    1.18 +
    1.19  
    1.20  (* bootstrap environment *)
    1.21  
    1.22  val bootstrap_values =
    1.23    ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
    1.24      "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
    1.25 -val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
    1.26  val bootstrap_structures =
    1.27    ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
    1.28      "Private_Output", "PolyML"] @ hidden_structures;