comparison src/elab_print.sml @ 162:06a98129b23f

Add datatype import constructor annotations; datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 12:30:04 -0400
parents 34ccd7d2bea8
children c7a6e6dbc318
comparison
equal deleted inserted replaced
161:a5ae7b3e37a4 162:06a98129b23f
344 space, 344 space,
345 string "=", 345 string "=",
346 space, 346 space,
347 p_con env c] 347 p_con env c]
348 | SgiDatatype x => p_datatype env x 348 | SgiDatatype x => p_datatype env x
349 | SgiDatatypeImp (x, _, m1, ms, x') => 349 | SgiDatatypeImp (x, _, m1, ms, x', _) =>
350 let 350 let
351 val m1x = #1 (E.lookupStrNamed env m1) 351 val m1x = #1 (E.lookupStrNamed env m1)
352 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 352 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
353 in 353 in
354 box [string "datatype", 354 box [string "datatype",
466 space, 466 space,
467 string "=", 467 string "=",
468 space, 468 space,
469 p_con env c] 469 p_con env c]
470 | DDatatype x => p_datatype env x 470 | DDatatype x => p_datatype env x
471 | DDatatypeImp (x, _, m1, ms, x') => 471 | DDatatypeImp (x, _, m1, ms, x', _) =>
472 let 472 let
473 val m1x = #1 (E.lookupStrNamed env m1) 473 val m1x = #1 (E.lookupStrNamed env m1)
474 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 474 handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
475 in 475 in
476 box [string "datatype", 476 box [string "datatype",