src/Pure/Isar/experiment.ML
author wenzelm
Fri, 03 Apr 2015 20:23:19 +0200
changeset 59919 fe1d8576b483
parent 59901 840d03805755
child 59923 b21c82422d65
permissions -rw-r--r--
clarified name space policy: show less stuff in usual print functions;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59901
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/experiment.ML
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
     3
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
     4
Target for specification experiments that are mostly private.
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
     5
*)
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
     6
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
     7
signature EXPERIMENT =
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
     8
sig
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
     9
  val experiment: Element.context_i list -> theory -> Binding.scope * local_theory
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    10
  val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    11
end;
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    12
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    13
structure Experiment: EXPERIMENT =
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    14
struct
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    15
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    16
fun gen_experiment add_locale elems thy =
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    17
  let
59919
fe1d8576b483 clarified name space policy: show less stuff in usual print functions;
wenzelm
parents: 59901
diff changeset
    18
    val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed;
fe1d8576b483 clarified name space policy: show less stuff in usual print functions;
wenzelm
parents: 59901
diff changeset
    19
    val (_, lthy) = thy |> add_locale experiment_name Binding.empty ([], []) elems;
59901
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    20
    val (scope, naming) =
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    21
      Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    22
    val naming' = naming |> Name_Space.private scope;
59919
fe1d8576b483 clarified name space policy: show less stuff in usual print functions;
wenzelm
parents: 59901
diff changeset
    23
    val lthy' = lthy
fe1d8576b483 clarified name space policy: show less stuff in usual print functions;
wenzelm
parents: 59901
diff changeset
    24
      |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')))
fe1d8576b483 clarified name space policy: show less stuff in usual print functions;
wenzelm
parents: 59901
diff changeset
    25
      |> Local_Theory.map_background_naming Name_Space.concealed;
59901
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    26
  in (scope, lthy') end;
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    27
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    28
val experiment = gen_experiment Expression.add_locale;
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    29
val experiment_cmd = gen_experiment Expression.add_locale_cmd;
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    30
840d03805755 added command 'experiment';
wenzelm
parents:
diff changeset
    31
end;