src/Tools/Code/code_printer.ML
changeset 55147 bce3dbc11f95
parent 55145 2bb3cd36bcf7
child 55148 7e1b7cb54114
     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: string -> Pretty.T -> Pretty.T
     1.8 -  val format: string list -> int -> Pretty.T -> string
     1.9 +  val markup_stmt: Code_Symbol.symbol -> Pretty.T -> Pretty.T
    1.10 +  val format: Code_Symbol.symbol 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) -> (string -> string)
    1.19 +  val intro_base_names_for: (string -> bool) -> (Code_Symbol.symbol -> 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 @@ -81,7 +81,7 @@
    1.24    val simple_const_syntax: simple_const_syntax -> const_syntax
    1.25    val complex_const_syntax: complex_const_syntax -> const_syntax
    1.26    val activate_const_syntax: theory -> literals
    1.27 -    -> string -> const_syntax -> Code_Thingol.naming -> activated_const_syntax * Code_Thingol.naming
    1.28 +    -> string -> const_syntax -> activated_const_syntax
    1.29    val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
    1.30      -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    1.31      -> (string -> activated_const_syntax option)
    1.32 @@ -125,17 +125,18 @@
    1.33  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
    1.34  fun indent i = Print_Mode.setmp [] (Pretty.indent i);
    1.35  
    1.36 -fun markup_stmt name = Print_Mode.setmp [code_presentationN]
    1.37 -  (Pretty.mark (code_presentationN, [(stmt_nameN, name)]));
    1.38 +fun markup_stmt sym = Print_Mode.setmp [code_presentationN]
    1.39 +  (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
    1.40  
    1.41  fun filter_presentation [] tree =
    1.42        Buffer.empty
    1.43        |> fold XML.add_content tree
    1.44 -  | filter_presentation presentation_names tree =
    1.45 +  | filter_presentation presentation_syms tree =
    1.46        let
    1.47 +        val presentation_idents = map Code_Symbol.marker presentation_syms
    1.48          fun is_selected (name, attrs) =
    1.49            name = code_presentationN
    1.50 -          andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN));
    1.51 +          andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN));
    1.52          fun add_content_with_space tree (is_first, buf) =
    1.53            buf
    1.54            |> not is_first ? Buffer.add "\n\n"
    1.55 @@ -198,8 +199,8 @@
    1.56  
    1.57  fun intro_base_names_for no_syntax deresolve ts =
    1.58    []
    1.59 -  |> fold Code_Thingol.add_constnames ts 
    1.60 -  |> intro_base_names no_syntax deresolve;
    1.61 +  |> fold Code_Thingol.add_constsyms ts 
    1.62 +  |> intro_base_names (fn Code_Symbol.Constant const => no_syntax const | _ => true) deresolve;
    1.63  
    1.64  
    1.65  (** pretty literals **)
    1.66 @@ -304,30 +305,31 @@
    1.67  datatype activated_const_syntax = Plain_const_syntax of int * string
    1.68    | Complex_const_syntax of activated_complex_const_syntax;
    1.69  
    1.70 -fun activate_const_syntax thy literals c (plain_const_syntax s) naming =
    1.71 -      (Plain_const_syntax (Code.args_number thy c, s), naming)
    1.72 -  | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f))) naming =
    1.73 -      fold_map (Code_Thingol.ensure_declared_const thy) cs naming
    1.74 -      |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
    1.75 +fun activate_const_syntax thy literals c (plain_const_syntax s) =
    1.76 +      Plain_const_syntax (Code.args_number thy c, s)
    1.77 +  | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f)))=
    1.78 +      Complex_const_syntax (n, f literals cs);
    1.79  
    1.80  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
    1.81 -    (app as ({ name = c, dom, ... }, ts)) =
    1.82 -  case const_syntax c of
    1.83 -    NONE => brackify fxy (print_app_expr some_thm vars app)
    1.84 -  | SOME (Plain_const_syntax (_, s)) =>
    1.85 -      brackify fxy (str s :: map (print_term some_thm vars BR) ts)
    1.86 -  | SOME (Complex_const_syntax (k, print)) =>
    1.87 -      let
    1.88 -        fun print' fxy ts =
    1.89 -          print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
    1.90 -      in
    1.91 -        if k = length ts
    1.92 -        then print' fxy ts
    1.93 -        else if k < length ts
    1.94 -        then case chop k ts of (ts1, ts2) =>
    1.95 -          brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
    1.96 -        else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
    1.97 -      end;
    1.98 +    (app as ({ sym, dom, ... }, ts)) =
    1.99 +  case sym of
   1.100 +    Code_Symbol.Constant const => (case const_syntax const of
   1.101 +      NONE => brackify fxy (print_app_expr some_thm vars app)
   1.102 +    | SOME (Plain_const_syntax (_, s)) =>
   1.103 +        brackify fxy (str s :: map (print_term some_thm vars BR) ts)
   1.104 +    | SOME (Complex_const_syntax (k, print)) =>
   1.105 +        let
   1.106 +          fun print' fxy ts =
   1.107 +            print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
   1.108 +        in
   1.109 +          if k = length ts
   1.110 +          then print' fxy ts
   1.111 +          else if k < length ts
   1.112 +          then case chop k ts of (ts1, ts2) =>
   1.113 +            brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
   1.114 +          else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
   1.115 +        end)
   1.116 +  | _ => brackify fxy (print_app_expr some_thm vars app);
   1.117  
   1.118  fun gen_print_bind print_term thm (fxy : fixity) pat vars =
   1.119    let