src/Pure/General/pretty.ML
changeset 62820 5c678ee5d34a
parent 62819 d3ff367a16a0
child 62823 751bcf0473a7
equal deleted inserted replaced
62819:d3ff367a16a0 62820:5c678ee5d34a
   393 fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
   393 fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
   394       make_block {markup = m, consistent = consistent, indent = FixedInt.toInt indent}
   394       make_block {markup = m, consistent = consistent, indent = FixedInt.toInt indent}
   395         (map from_ML prts)
   395         (map from_ML prts)
   396   | from_ML (ML_Pretty.Break (force, wd, ind)) =
   396   | from_ML (ML_Pretty.Break (force, wd, ind)) =
   397       Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
   397       Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
   398   | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt (force_nat len));
   398   | from_ML (ML_Pretty.String (s, len)) = Str (s, force_nat (FixedInt.toInt len));
   399 
   399 
   400 val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
   400 val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
   401 val from_polyml = ML_Pretty.from_polyml #> from_ML;
   401 val from_polyml = ML_Pretty.from_polyml #> from_ML;
   402 
   402 
   403 end;
   403 end;