1.1 --- a/etc/settings	Fri Apr 29 00:52:12 2005 +0200
     1.2 +++ b/etc/settings	Fri Apr 29 08:03:01 2005 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4  
     1.5  
     1.6  ###
     1.7 -### Compilation options for isatool usedir
     1.8 +### Compilation options for isatool usedir[B
     1.9  ### (as on command line)
    1.10  ###
    1.11  

     2.1 --- a/src/Pure/Isar/isar_output.ML	Fri Apr 29 00:52:12 2005 +0200
     2.2 +++ b/src/Pure/Isar/isar_output.ML	Fri Apr 29 08:03:01 2005 +0200
     2.3 @@ -29,6 +29,7 @@
     2.4        (Toplevel.transition * (Toplevel.state -> Toplevel.state -> Buffer.T -> Buffer.T)) list * Buffer.T
     2.5    val output_with: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
     2.6      Proof.context -> 'a -> string
     2.7 +  val put_style: string -> (Term.term -> Term.term) -> theory -> theory
     2.8  end;
     2.9  
    2.10  structure IsarOutput: ISAR_OUTPUT =
    2.11 @@ -310,6 +311,31 @@
    2.12    ("source", Library.setmp source o boolean),
    2.13    ("goals_limit", Library.setmp goals_limit o integer)];
    2.14  
    2.15 +(* style data *)
    2.16 +
    2.17 +exception Style of string;
    2.18 +
    2.19 +structure StyleArgs =
    2.20 +struct
    2.21 +  val name = "Isar/style";
    2.22 +  type T = (string * (Term.term -> Term.term)) list;
    2.23 +  val empty = [];
    2.24 +  val copy = I;
    2.25 +  val prep_ext = I;
    2.26 +  fun merge (a1, a2) = Library.foldl Library.overwrite (a1, a2);
    2.27 +    (* piecewise update of a1 by a2 *)
    2.28 +  fun print _ _ = raise (Style "cannot print style (not implemented)");
    2.29 +end;
    2.30 +
    2.31 +structure Style = TheoryDataFun(StyleArgs);
    2.32 +
    2.33 +fun get_style thy name =
    2.34 +  case Library.assoc_string ((Style.get thy), name)
    2.35 +    of NONE => raise (Style ("no style named " ^ name))
    2.36 +     | SOME style => style
    2.37 +
    2.38 +fun put_style name style thy =
    2.39 +  Style.put (Library.overwrite ((Style.get thy), (name, style))) thy;
    2.40  
    2.41  (* commands *)
    2.42  
    2.43 @@ -346,8 +372,24 @@
    2.44  
    2.45  fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt;
    2.46  
    2.47 +fun pretty_term_typ ctxt term = Pretty.block [
    2.48 +  ((ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt) term),
    2.49 +  (Pretty.str "\\<Colon>") (* q'n'd *),
    2.50 +  ((ProofContext.pretty_typ ctxt o Term.type_of o ProofContext.extern_skolem ctxt) term)
    2.51 +  ]
    2.52 +
    2.53 +fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.type_of o ProofContext.extern_skolem ctxt;
    2.54 +
    2.55 +fun pretty_term_const ctxt term = case Sign.const_type (ProofContext.sign_of ctxt) (Term.string_of_term term) of 
    2.56 +  NONE => raise (Output.ERROR_MESSAGE ("Not a defined constant: " ^ (Term.string_of_term term)))
    2.57 +  | (SOME _) => (ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt) term;
    2.58 +
    2.59  fun pretty_thm ctxt = pretty_term ctxt o Thm.prop_of;
    2.60  
    2.61 +fun pretty_term_style ctxt (name, term) = pretty_term ctxt ((get_style (ProofContext.theory_of ctxt) name) term);
    2.62 +
    2.63 +fun pretty_thm_style ctxt (name, thm) = pretty_term_style ctxt (name, Thm.prop_of thm);
    2.64 +
    2.65  fun lhs_of (Const ("==",_) $ t $ _) = t
    2.66    | lhs_of (Const ("Trueprop",_) $ t) = lhs_of t
    2.67    | lhs_of (Const ("==>",_) $ _ $ t) = lhs_of t
    2.68 @@ -385,10 +427,15 @@
    2.69  
    2.70  val _ = add_commands
    2.71   [("thm", args Attrib.local_thmss (output_seq_with pretty_thm)),
    2.72 +  ("thm_style", args ((Scan.lift Args.name) -- Attrib.local_thm) (output_with pretty_thm_style)),
    2.73    ("lhs", args Attrib.local_thmss (output_seq_with pretty_lhs)),
    2.74    ("rhs", args Attrib.local_thmss (output_seq_with pretty_rhs)),
    2.75    ("prop", args Args.local_prop (output_with pretty_term)),
    2.76    ("term", args Args.local_term (output_with pretty_term)),
    2.77 +  ("term_style", args ((Scan.lift Args.name) -- Args.local_term) (output_with pretty_term_style)),
    2.78 +  ("term_type", args Args.local_term (output_with pretty_term_typ)),
    2.79 +  ("typeof", args Args.local_term (output_with pretty_term_typeof)),
    2.80 +  ("const", args Args.local_term (output_with pretty_term_const)),
    2.81    ("typ", args Args.local_typ_raw (output_with ProofContext.pretty_typ)),
    2.82    ("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
    2.83    ("goals", output_goals true),
    2.84 @@ -396,4 +443,7 @@
    2.85    ("prf", args Attrib.local_thmss (output_with (pretty_prf false))),
    2.86    ("full_prf", args Attrib.local_thmss (output_with (pretty_prf true)))];
    2.87  
    2.88 +val _ = Context.add_setup [Style.init];
    2.89 +
    2.90  end;
    2.91 +