1.1 --- a/src/Pure/Isar/named_target.ML	Wed Sep 22 11:46:28 2010 +0200
     1.2 +++ b/src/Pure/Isar/named_target.ML	Wed Sep 22 12:22:47 2010 +0200
     1.3 @@ -21,12 +21,7 @@
     1.4  
     1.5  datatype target = Target of {target: string, is_locale: bool, is_class: bool};
     1.6  
     1.7 -fun make_target target is_locale is_class =
     1.8 -  Target {target = target, is_locale = is_locale, is_class = is_class};
     1.9 -
    1.10 -val global_target = Target {target = "", is_locale = false, is_class = false};
    1.11 -
    1.12 -fun named_target _ "" = global_target
    1.13 +fun named_target _ "" = Target {target = "", is_locale = false, is_class = false}
    1.14    | named_target thy locale =
    1.15        if Locale.defined thy locale
    1.16        then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale}
    1.17 @@ -103,7 +98,7 @@
    1.18      #> Class.const target ((b, mx), (type_params, lhs))
    1.19      #> pair (lhs, def))
    1.20  
    1.21 -fun target_foundation (ta as Target {target, is_locale, is_class, ...}) =
    1.22 +fun target_foundation (ta as Target {is_locale, is_class, ...}) =
    1.23    if is_class then class_foundation ta
    1.24    else if is_locale then locale_foundation ta
    1.25    else Generic_Target.theory_foundation;
    1.26 @@ -122,7 +117,7 @@
    1.27      |> Local_Theory.target (Locale.add_thmss locale kind local_facts')
    1.28    end
    1.29  
    1.30 -fun target_notes (ta as Target {target, is_locale, ...}) =
    1.31 +fun target_notes (Target {target, is_locale, ...}) =
    1.32    if is_locale then locale_notes target
    1.33      else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
    1.34  
    1.35 @@ -148,7 +143,7 @@
    1.36  
    1.37  (* pretty *)
    1.38  
    1.39 -fun pretty_thy ctxt target is_class =
    1.40 +fun pretty (Target {target, is_locale, is_class, ...}) ctxt =
    1.41    let
    1.42      val thy = ProofContext.theory_of ctxt;
    1.43      val target_name =
    1.44 @@ -161,57 +156,50 @@
    1.45      val elems =
    1.46        (if null fixes then [] else [Element.Fixes fixes]) @
    1.47        (if null assumes then [] else [Element.Assumes assumes]);
    1.48 +    val body_elems =  if not is_locale then []
    1.49 +      else if null elems then [Pretty.block target_name]
    1.50 +      else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
    1.51 +        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
    1.52    in
    1.53 -    if target = "" then []
    1.54 -    else if null elems then [Pretty.block target_name]
    1.55 -    else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
    1.56 -      map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
    1.57 +    Pretty.block [Pretty.command "theory", Pretty.brk 1,
    1.58 +      Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems
    1.59    end;
    1.60  
    1.61 -fun pretty (Target {target, is_class, ...}) ctxt =
    1.62 -  Pretty.block [Pretty.command "theory", Pretty.brk 1,
    1.63 -      Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] ::
    1.64 -    pretty_thy ctxt target is_class;
    1.65 -
    1.66  
    1.67  (* init *)
    1.68  
    1.69 -local
    1.70 -
    1.71  fun init_context (Target {target, is_locale, is_class}) =
    1.72    if not is_locale then ProofContext.init_global
    1.73    else if not is_class then Locale.init target
    1.74    else Class.init target;
    1.75  
    1.76 -fun init_target (ta as Target {target, ...}) thy =
    1.77 -  thy
    1.78 -  |> init_context ta
    1.79 -  |> Data.put (SOME ta)
    1.80 -  |> Local_Theory.init NONE (Long_Name.base_name target)
    1.81 -     {define = Generic_Target.define (target_foundation ta),
    1.82 -      notes = Generic_Target.notes (target_notes ta),
    1.83 -      abbrev = Generic_Target.abbrev (target_abbrev ta),
    1.84 -      declaration = fn pervasive => target_declaration ta
    1.85 -        { syntax = false, pervasive = pervasive },
    1.86 -      syntax_declaration = fn pervasive => target_declaration ta
    1.87 -        { syntax = true, pervasive = pervasive },
    1.88 -      pretty = pretty ta,
    1.89 -      exit = Local_Theory.target_of};
    1.90 +fun init target thy =
    1.91 +  let
    1.92 +    val ta = named_target thy target;
    1.93 +  in
    1.94 +    thy
    1.95 +    |> init_context ta
    1.96 +    |> Data.put (SOME ta)
    1.97 +    |> Local_Theory.init NONE (Long_Name.base_name target)
    1.98 +       {define = Generic_Target.define (target_foundation ta),
    1.99 +        notes = Generic_Target.notes (target_notes ta),
   1.100 +        abbrev = Generic_Target.abbrev (target_abbrev ta),
   1.101 +        declaration = fn pervasive => target_declaration ta
   1.102 +          { syntax = false, pervasive = pervasive },
   1.103 +        syntax_declaration = fn pervasive => target_declaration ta
   1.104 +          { syntax = true, pervasive = pervasive },
   1.105 +        pretty = pretty ta,
   1.106 +        exit = Local_Theory.target_of}
   1.107 +  end;
   1.108  
   1.109 -in
   1.110 -
   1.111 -fun init target thy = init_target (named_target thy target) thy;
   1.112 +val theory_init = init "";
   1.113  
   1.114  fun reinit lthy =
   1.115    (case peek lthy of
   1.116      SOME {target, ...} => init target o Local_Theory.exit_global
   1.117    | NONE => error "Not in a named target");
   1.118  
   1.119 -val theory_init = init_target global_target;
   1.120 -
   1.121  fun context_cmd "-" thy = init "" thy
   1.122    | context_cmd target thy = init (Locale.intern thy target) thy;
   1.123  
   1.124  end;
   1.125 -
   1.126 -end;