src/Pure/Isar/experiment.ML
changeset 59919 fe1d8576b483
parent 59901 840d03805755
child 59923 b21c82422d65
equal deleted inserted replaced
59918:d01e6d159c33 59919:fe1d8576b483
    13 structure Experiment: EXPERIMENT =
    13 structure Experiment: EXPERIMENT =
    14 struct
    14 struct
    15 
    15 
    16 fun gen_experiment add_locale elems thy =
    16 fun gen_experiment add_locale elems thy =
    17   let
    17   let
    18     val (_, lthy) = thy
    18     val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed;
    19       |> add_locale (Binding.name ("experiment" ^ serial_string ())) Binding.empty ([], []) elems;
    19     val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems;
    20     val (scope, naming) =
    20     val (scope, naming) =
    21       Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
    21       Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
    22     val naming' = naming |> Name_Space.private scope;
    22     val naming' = naming |> Name_Space.private scope;
    23     val lthy' = lthy |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')));
    23     val lthy' = lthy
       
    24       |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')))
       
    25       |> Local_Theory.map_background_naming Name_Space.concealed;
    24   in (scope, lthy') end;
    26   in (scope, lthy') end;
    25 
    27 
    26 val experiment = gen_experiment Expression.add_locale;
    28 val experiment = gen_experiment Expression.add_locale;
    27 val experiment_cmd = gen_experiment Expression.add_locale_cmd;
    29 val experiment_cmd = gen_experiment Expression.add_locale_cmd;
    28 
    30