src/Pure/Isar/proof_context.ML
changeset 20367 ba1c262c7625
parent 20330 6192478fdba5
child 20575 6b1c69265331
equal deleted inserted replaced
20366:867696dc64fc 20367:ba1c262c7625
    15   val consts_of: Proof.context -> Consts.T
    15   val consts_of: Proof.context -> Consts.T
    16   val set_syntax_mode: string * bool -> Proof.context -> Proof.context
    16   val set_syntax_mode: string * bool -> Proof.context -> Proof.context
    17   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    17   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    18   val fact_index_of: Proof.context -> FactIndex.T
    18   val fact_index_of: Proof.context -> FactIndex.T
    19   val transfer: theory -> Proof.context -> Proof.context
    19   val transfer: theory -> Proof.context -> Proof.context
    20   val map_theory: (theory -> theory) -> Proof.context -> Proof.context
    20   val theory: (theory -> theory) -> Proof.context -> Proof.context
       
    21   val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
    21   val pretty_term: Proof.context -> term -> Pretty.T
    22   val pretty_term: Proof.context -> term -> Pretty.T
    22   val pretty_typ: Proof.context -> typ -> Pretty.T
    23   val pretty_typ: Proof.context -> typ -> Pretty.T
    23   val pretty_sort: Proof.context -> sort -> Pretty.T
    24   val pretty_sort: Proof.context -> sort -> Pretty.T
    24   val pretty_classrel: Proof.context -> class list -> Pretty.T
    25   val pretty_classrel: Proof.context -> class list -> Pretty.T
    25   val pretty_arity: Proof.context -> arity -> Pretty.T
    26   val pretty_arity: Proof.context -> arity -> Pretty.T
   228 val fact_index_of = #2 o thms_of;
   229 val fact_index_of = #2 o thms_of;
   229 
   230 
   230 val cases_of = #cases o rep_context;
   231 val cases_of = #cases o rep_context;
   231 
   232 
   232 
   233 
   233 (* transfer *)
   234 (* theory transfer *)
   234 
   235 
   235 fun transfer_syntax thy =
   236 fun transfer_syntax thy =
   236   map_syntax (LocalSyntax.rebuild thy) #>
   237   map_syntax (LocalSyntax.rebuild thy) #>
   237   map_consts (fn consts as (global_consts, local_consts) =>
   238   map_consts (fn consts as (global_consts, local_consts) =>
   238     let val thy_consts = Sign.consts_of thy in
   239     let val thy_consts = Sign.consts_of thy in
   240       else (thy_consts, Consts.merge (thy_consts, local_consts))
   241       else (thy_consts, Consts.merge (thy_consts, local_consts))
   241     end);
   242     end);
   242 
   243 
   243 fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
   244 fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy;
   244 
   245 
   245 fun map_theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
   246 fun theory f ctxt = transfer (f (theory_of ctxt)) ctxt;
       
   247 
       
   248 fun theory_result f ctxt =
       
   249   let val (res, thy') = f (theory_of ctxt)
       
   250   in (res, ctxt |> transfer thy') end;
   246 
   251 
   247 
   252 
   248 
   253 
   249 (** pretty printing **)
   254 (** pretty printing **)
   250 
   255 
  1100 val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;
  1105 val print_cases = Pretty.writeln o Pretty.chunks o pretty_cases;
  1101 
  1106 
  1102 
  1107 
  1103 (* core context *)
  1108 (* core context *)
  1104 
  1109 
  1105 val prems_limit = ref 10;
  1110 val prems_limit = ref ~1;
  1106 
  1111 
  1107 fun pretty_ctxt ctxt =
  1112 fun pretty_ctxt ctxt =
  1108   if ! prems_limit < 0 andalso not (! debug) then []
  1113   if ! prems_limit < 0 andalso not (! debug) then []
  1109   else
  1114   else
  1110     let
  1115     let
  1126       val prt_fixes = if null fixes then []
  1131       val prt_fixes = if null fixes then []
  1127         else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
  1132         else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
  1128           Pretty.commas (map prt_fix fixes))];
  1133           Pretty.commas (map prt_fix fixes))];
  1129 
  1134 
  1130       (*prems*)
  1135       (*prems*)
  1131       val limit = ! prems_limit;
       
  1132       val prems = Assumption.prems_of ctxt;
  1136       val prems = Assumption.prems_of ctxt;
  1133       val len = length prems;
  1137       val len = length prems;
       
  1138       val suppressed = len - ! prems_limit;
  1134       val prt_prems = if null prems then []
  1139       val prt_prems = if null prems then []
  1135         else [Pretty.big_list "prems:" ((if len <= limit then [] else [Pretty.str "..."]) @
  1140         else [Pretty.big_list "prems:" ((if suppressed <= 0 then [] else [Pretty.str "..."]) @
  1136           map (pretty_thm ctxt) (Library.drop (len - limit, prems)))];
  1141           map (pretty_thm ctxt) (Library.drop (suppressed, prems)))];
  1137     in prt_structs @ prt_fixes @ prt_prems end;
  1142     in prt_structs @ prt_fixes @ prt_prems end;
  1138 
  1143 
  1139 
  1144 
  1140 (* main context *)
  1145 (* main context *)
  1141 
  1146