src/Pure/PIDE/xml.ML
changeset 62663 bea354f6ff21
parent 61707 d5ddd022a451
child 62819 d3ff367a16a0
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
   168 val output = Buffer.output o buffer_of ~1;
   168 val output = Buffer.output o buffer_of ~1;
   169 
   169 
   170 fun pretty depth tree =
   170 fun pretty depth tree =
   171   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
   171   Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
   172 
   172 
       
   173 val _ =
       
   174   PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
       
   175 
   173 
   176 
   174 
   177 
   175 (** XML parsing **)
   178 (** XML parsing **)
   176 
   179 
   177 local
   180 local