src/Tools/code/code_printer.ML
changeset 31665 a1f4d3b3f6c8
parent 31056 01ac77eb660b
equal deleted inserted replaced
31643:b040f1679f77 31665:a1f4d3b3f6c8
    43   val NOBR: fixity
    43   val NOBR: fixity
    44   val INFX: int * lrx -> fixity
    44   val INFX: int * lrx -> fixity
    45   val APP: fixity
    45   val APP: fixity
    46   val brackify: fixity -> Pretty.T list -> Pretty.T
    46   val brackify: fixity -> Pretty.T list -> Pretty.T
    47   val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
    47   val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
       
    48   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
    48 
    49 
    49   type itype = Code_Thingol.itype
    50   type itype = Code_Thingol.itype
    50   type iterm = Code_Thingol.iterm
    51   type iterm = Code_Thingol.iterm
    51   type const = Code_Thingol.const
    52   type const = Code_Thingol.const
    52   type dict = Code_Thingol.dict
    53   type dict = Code_Thingol.dict
   173   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
   174   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
   174 
   175 
   175 fun brackify_infix infx fxy_ctxt =
   176 fun brackify_infix infx fxy_ctxt =
   176   gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
   177   gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
   177 
   178 
       
   179 fun brackify_block fxy_ctxt p1 ps p2 =
       
   180   let val p = Pretty.block_enclose (p1, p2) ps
       
   181   in if fixity BR fxy_ctxt
       
   182     then Pretty.enclose "(" ")" [p]
       
   183     else p
       
   184   end;
       
   185 
   178 
   186 
   179 (* generic syntax *)
   187 (* generic syntax *)
   180 
   188 
   181 type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
   189 type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
   182   -> fixity -> itype list -> Pretty.T);
   190   -> fixity -> itype list -> Pretty.T);