src/Pure/display.ML
changeset 24774 bc31c318e673
parent 24665 e5bea50b9b89
child 24848 5dbbd33c3236
equal deleted inserted replaced
24773:ec3a04e6f1a9 24774:bc31c318e673
   207     val extern_const = NameSpace.extern (#1 constants);
   207     val extern_const = NameSpace.extern (#1 constants);
   208     val {classes, default, types, witness, ...} = Type.rep_tsig tsig;
   208     val {classes, default, types, witness, ...} = Type.rep_tsig tsig;
   209     val (class_space, class_algebra) = classes;
   209     val (class_space, class_algebra) = classes;
   210     val {classes, arities} = Sorts.rep_algebra class_algebra;
   210     val {classes, arities} = Sorts.rep_algebra class_algebra;
   211 
   211 
   212     fun prune xs = if verbose then xs else filter_out (can Name.dest_internal o fst) xs;
   212     val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
   213     fun prune' xs = if verbose then xs else filter_out (can Name.dest_internal o fst o fst) xs;
   213     val tdecls = NameSpace.dest_table types;
   214     fun dest_table tab = prune (NameSpace.dest_table tab);
   214     val arties = NameSpace.dest_table (Sign.type_space thy, arities);
   215     fun extern_table tab = prune (NameSpace.extern_table tab);
   215 
   216 
   216     fun prune_const c = not verbose andalso
   217     val clsses = dest_table (class_space, Symtab.make (Graph.dest classes));
   217       member (op =) (Consts.the_tags consts c) Markup.property_internal;
   218     val tdecls = dest_table types;
   218     val cnsts = NameSpace.extern_table (#1 constants,
   219     val arties = dest_table (Sign.type_space thy, arities);
   219       Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
   220     val cnsts = extern_table constants;
   220 
   221     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   221     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   222     val abbrevs = map_filter (fn (c, (ty, SOME (t, _))) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   222     val abbrevs = map_filter (fn (c, (ty, SOME (t, _))) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   223     val cnstrs = extern_table constraints;
   223     val cnstrs = NameSpace.extern_table constraints;
   224     val axms = extern_table axioms;
   224 
   225     val oras = extern_table oracles;
   225     val axms = NameSpace.extern_table axioms;
   226 
   226     val oras = NameSpace.extern_table oracles;
   227     val (reds0, (reds1, reds2)) = prune' reducts |> map (fn (lhs, rhs) =>
   227 
   228         (apfst extern_const lhs, map (apfst extern_const) (prune rhs)))
   228     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       
   229       |> map (fn (lhs, rhs) =>
       
   230         (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
   229       |> sort_wrt (#1 o #1)
   231       |> sort_wrt (#1 o #1)
   230       |> List.partition (null o #2)
   232       |> List.partition (null o #2)
   231       ||> List.partition (Defs.plain_args o #2 o #1);
   233       ||> List.partition (Defs.plain_args o #2 o #1);
   232     val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
   234     val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
   233   in
   235   in