equal
deleted
inserted
replaced
107 |
107 |
108 val mode = Unsynchronized.ref ([] : string list); (* FIXME proper functional argument *) |
108 val mode = Unsynchronized.ref ([] : string list); (* FIXME proper functional argument *) |
109 |
109 |
110 val margin = Unsynchronized.ref 80; |
110 val margin = Unsynchronized.ref 80; |
111 |
111 |
112 fun string_of p = (Pretty.string_of |> |
112 fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p; |
113 PrintMode.setmp [] |> |
|
114 Pretty.setmp_margin_CRITICAL (!margin)) p; |
|
115 |
113 |
116 val str = PrintMode.setmp [] Pretty.str; |
114 val str = PrintMode.setmp [] Pretty.str; |
117 |
115 |
118 (**** Mixfix syntax ****) |
116 (**** Mixfix syntax ****) |
119 |
117 |