src/Tools/Code/code_printer.ML
changeset 43947 9b00f09f7721
parent 43326 47cf4bc789aa
child 44788 8b935f1b3cf8
     1.1 --- a/src/Tools/Code/code_printer.ML	Sat Jul 23 16:12:12 2011 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Sat Jul 23 16:37:17 2011 +0200
     1.3 @@ -101,7 +101,8 @@
     1.4  
     1.5  (** generic nonsense *)
     1.6  
     1.7 -fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
     1.8 +fun eqn_error (SOME thm) s =
     1.9 +      error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
    1.10    | eqn_error NONE s = error s;
    1.11  
    1.12  val code_presentationN = "code_presentation";
    1.13 @@ -132,10 +133,10 @@
    1.14  
    1.15  fun filter_presentation [] tree =
    1.16        Buffer.empty
    1.17 -      |> fold XML.add_content tree 
    1.18 +      |> fold XML.add_content tree
    1.19    | filter_presentation presentation_names tree =
    1.20        let
    1.21 -        fun is_selected (name, attrs) = 
    1.22 +        fun is_selected (name, attrs) =
    1.23            name = code_presentationN
    1.24            andalso member (op =) presentation_names (the (Properties.get attrs stmt_nameN));
    1.25          fun add_content_with_space tree (is_first, buf) =
    1.26 @@ -169,8 +170,9 @@
    1.27      val namemap' = fold2 (curry Symtab.update) names names' namemap;
    1.28    in (namemap', namectxt') end;
    1.29  
    1.30 -fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
    1.31 - of SOME name' => name'
    1.32 +fun lookup_var (namemap, _) name =
    1.33 +  case Symtab.lookup namemap name of
    1.34 +    SOME name' => name'
    1.35    | NONE => error ("Invalid name in context: " ^ quote name);
    1.36  
    1.37  val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
    1.38 @@ -190,7 +192,7 @@
    1.39      val vars' = intro_vars fished3 vars;
    1.40    in map (lookup_var vars') fished3 end;
    1.41  
    1.42 -fun intro_base_names no_syntax deresolve names = names 
    1.43 +fun intro_base_names no_syntax deresolve names = names
    1.44    |> map_filter (fn name => if no_syntax name then
    1.45        let val name' = deresolve name in
    1.46          if Long_Name.is_qualified name' then NONE else SOME name'
    1.47 @@ -297,7 +299,8 @@
    1.48    | requires_args (complex_const_syntax (k, _)) = k;
    1.49  
    1.50  fun simple_const_syntax syn =
    1.51 -  complex_const_syntax (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
    1.52 +  complex_const_syntax
    1.53 +    (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
    1.54  
    1.55  type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    1.56    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
    1.57 @@ -311,20 +314,24 @@
    1.58        fold_map (Code_Thingol.ensure_declared_const thy) cs naming
    1.59        |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
    1.60  
    1.61 -fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy (app as ((c, (_, function_typs)), ts)) =
    1.62 -  case const_syntax c
    1.63 -   of NONE => brackify fxy (print_app_expr some_thm vars app)
    1.64 -    | SOME (Plain_const_syntax (_, s)) => brackify fxy (str s :: map (print_term some_thm vars BR) ts)
    1.65 -    | SOME (Complex_const_syntax (k, print)) =>
    1.66 -        let
    1.67 -          fun print' fxy ts = print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
    1.68 -        in if k = length ts
    1.69 -          then print' fxy ts
    1.70 +fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
    1.71 +    (app as ((c, (_, function_typs)), ts)) =
    1.72 +  case const_syntax c of
    1.73 +    NONE => brackify fxy (print_app_expr some_thm vars app)
    1.74 +  | SOME (Plain_const_syntax (_, s)) =>
    1.75 +      brackify fxy (str s :: map (print_term some_thm vars BR) ts)
    1.76 +  | SOME (Complex_const_syntax (k, print)) =>
    1.77 +      let
    1.78 +        fun print' fxy ts =
    1.79 +          print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
    1.80 +      in
    1.81 +        if k = length ts
    1.82 +        then print' fxy ts
    1.83          else if k < length ts
    1.84 -          then case chop k ts of (ts1, ts2) =>
    1.85 -            brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
    1.86 -          else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
    1.87 -        end;
    1.88 +        then case chop k ts of (ts1, ts2) =>
    1.89 +          brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
    1.90 +        else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
    1.91 +      end;
    1.92  
    1.93  fun gen_print_bind print_term thm (fxy : fixity) pat vars =
    1.94    let
    1.95 @@ -377,12 +384,14 @@
    1.96             (   $$ "'" |-- sym_any
    1.97              || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
    1.98                   sym_any) >> (String o implode)));
    1.99 -  in case Scan.finite Symbol.stopper parse (Symbol.explode s)
   1.100 -   of ((false, [String s]), []) => mk_plain s
   1.101 +    fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s)
   1.102 +      | err _ (_, SOME msg) = msg;
   1.103 +  in
   1.104 +    case Scan.finite Symbol.stopper parse (Symbol.explode s) of
   1.105 +      ((false, [String s]), []) => mk_plain s
   1.106      | ((_, p as [_]), []) => mk_complex (mk_mixfix prep_arg (NOBR, p))
   1.107      | ((b, p as _ :: _ :: _), []) => mk_complex (mk_mixfix prep_arg (if b then NOBR else BR, p))
   1.108 -    | _ => Scan.!!
   1.109 -        (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
   1.110 +    | _ => Scan.!! (err s) Scan.fail ()
   1.111    end;
   1.112  
   1.113  val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");