Named_Target.init: empty string represents theory target
authorhaftmann
Thu Aug 12 13:28:18 2010 +0200 (2010-08-12 ago)
changeset 38389d7d915bae307
parent 38388 94d5624dd1f7
child 38390 cb72d89bb444
Named_Target.init: empty string represents theory target
src/HOL/Statespace/state_space.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Thu Aug 12 13:23:46 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Thu Aug 12 13:28:18 2010 +0200
     1.3 @@ -466,7 +466,7 @@
     1.4                  (suffix valuetypesN full_name,(("",false),Expression.Named  []))],[]) fixestate
     1.5       |> ProofContext.theory_of 
     1.6       |> fold interprete_parent parents
     1.7 -     |> add_declaration (SOME full_name) (declare_declinfo components')
     1.8 +     |> add_declaration full_name (declare_declinfo components')
     1.9    end;
    1.10  
    1.11  
     2.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:23:46 2010 +0200
     2.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:28:18 2010 +0200
     2.3 @@ -290,7 +290,7 @@
     2.4         Context.theory_map (Locale.add_registration (class, base_morph)
     2.5           (Option.map (rpair true) eq_morph) export_morph)
     2.6      #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     2.7 -    |> Named_Target.init (SOME class)
     2.8 +    |> Named_Target.init class
     2.9      |> pair class
    2.10    end;
    2.11  
    2.12 @@ -323,7 +323,7 @@
    2.13      fun after_qed some_wit =
    2.14        ProofContext.theory (Class.register_subclass (sub, sup)
    2.15          some_dep_morph some_wit export)
    2.16 -      #> ProofContext.theory_of #> Named_Target.init (SOME sub);
    2.17 +      #> ProofContext.theory_of #> Named_Target.init sub;
    2.18    in do_proof after_qed some_prop goal_ctxt end;
    2.19  
    2.20  fun user_proof after_qed some_prop =
     3.1 --- a/src/Pure/Isar/expression.ML	Thu Aug 12 13:23:46 2010 +0200
     3.2 +++ b/src/Pure/Isar/expression.ML	Thu Aug 12 13:28:18 2010 +0200
     3.3 @@ -775,7 +775,7 @@
     3.4      val loc_ctxt = thy'
     3.5        |> Locale.register_locale binding (extraTs, params)
     3.6            (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
     3.7 -      |> Named_Target.init (SOME name)
     3.8 +      |> Named_Target.init name
     3.9        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    3.10  
    3.11    in (name, loc_ctxt) end;
    3.12 @@ -870,7 +870,7 @@
    3.13  fun gen_sublocale prep_expr intern raw_target expression thy =
    3.14    let
    3.15      val target = intern thy raw_target;
    3.16 -    val target_ctxt = Named_Target.init (SOME target) thy;
    3.17 +    val target_ctxt = Named_Target.init target thy;
    3.18      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    3.19      fun after_qed witss = ProofContext.theory
    3.20        (fold (fn ((dep, morph), wits) => Locale.add_dependency
     4.1 --- a/src/Pure/Isar/named_target.ML	Thu Aug 12 13:23:46 2010 +0200
     4.2 +++ b/src/Pure/Isar/named_target.ML	Thu Aug 12 13:28:18 2010 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  signature NAMED_TARGET =
     4.5  sig
     4.6    val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
     4.7 -  val init: string option -> theory -> local_theory
     4.8 +  val init: string -> theory -> local_theory
     4.9    val theory_init: theory -> local_theory
    4.10    val context_cmd: xstring -> theory -> local_theory
    4.11  end;
    4.12 @@ -25,8 +25,8 @@
    4.13  
    4.14  val global_target = Target {target = "", is_locale = false, is_class = false};
    4.15  
    4.16 -fun named_target _ NONE = global_target
    4.17 -  | named_target thy (SOME locale) =
    4.18 +fun named_target _ "" = global_target
    4.19 +  | named_target thy locale =
    4.20        if Locale.defined thy locale
    4.21        then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
    4.22        else error ("No such locale: " ^ quote locale);
    4.23 @@ -205,8 +205,8 @@
    4.24  
    4.25  val theory_init = init_target global_target;
    4.26  
    4.27 -fun context_cmd "-" thy = init NONE thy
    4.28 -  | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
    4.29 +fun context_cmd "-" thy = init "" thy
    4.30 +  | context_cmd target thy = init (Locale.intern thy target) thy;
    4.31  
    4.32  end;
    4.33  
     5.1 --- a/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:23:46 2010 +0200
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Aug 12 13:28:18 2010 +0200
     5.3 @@ -112,8 +112,7 @@
     5.4  fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
     5.5    | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
     5.6    | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let
     5.7 -        val target_name = #target (Named_Target.peek lthy);
     5.8 -        val target = if target_name = "" then NONE else SOME target_name;
     5.9 +        val target = #target (Named_Target.peek lthy);
    5.10        in Context.Proof (Named_Target.init target (loc_exit lthy')) end;
    5.11  
    5.12