src/Tools/Code/code_printer.ML
changeset 55150 0940309ed8f1
parent 55148 7e1b7cb54114
child 55153 eedd549de3ef
     1.1 --- a/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -25,8 +25,8 @@
     1.4    val semicolon: Pretty.T list -> Pretty.T
     1.5    val doublesemicolon: Pretty.T list -> Pretty.T
     1.6    val indent: int -> Pretty.T -> Pretty.T
     1.7 -  val markup_stmt: Code_Symbol.symbol -> Pretty.T -> Pretty.T
     1.8 -  val format: Code_Symbol.symbol list -> int -> Pretty.T -> string
     1.9 +  val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
    1.10 +  val format: Code_Symbol.T list -> int -> Pretty.T -> string
    1.11  
    1.12    val first_upper: string -> string
    1.13    val first_lower: string -> string
    1.14 @@ -36,7 +36,7 @@
    1.15    val lookup_var: var_ctxt -> string -> string
    1.16    val intro_base_names: (string -> bool) -> (string -> string)
    1.17      -> string list -> var_ctxt -> var_ctxt
    1.18 -  val intro_base_names_for: (string -> bool) -> (Code_Symbol.symbol -> string)
    1.19 +  val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string)
    1.20      -> iterm list -> var_ctxt -> var_ctxt
    1.21    val aux_params: var_ctxt -> iterm list list -> string list
    1.22  
    1.23 @@ -94,6 +94,7 @@
    1.24  structure Code_Printer : CODE_PRINTER =
    1.25  struct
    1.26  
    1.27 +open Basic_Code_Symbol;
    1.28  open Code_Thingol;
    1.29  
    1.30  (** generic nonsense *)
    1.31 @@ -200,7 +201,7 @@
    1.32  fun intro_base_names_for no_syntax deresolve ts =
    1.33    []
    1.34    |> fold Code_Thingol.add_constsyms ts 
    1.35 -  |> intro_base_names (fn Code_Symbol.Constant const => no_syntax const | _ => true) deresolve;
    1.36 +  |> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve;
    1.37  
    1.38  
    1.39  (** pretty literals **)
    1.40 @@ -313,7 +314,7 @@
    1.41  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
    1.42      (app as ({ sym, dom, ... }, ts)) =
    1.43    case sym of
    1.44 -    Code_Symbol.Constant const => (case const_syntax const of
    1.45 +    Constant const => (case const_syntax const of
    1.46        NONE => brackify fxy (print_app_expr some_thm vars app)
    1.47      | SOME (Plain_const_syntax (_, s)) =>
    1.48          brackify fxy (str s :: map (print_term some_thm vars BR) ts)