summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
authorKathy Gray2014-11-10 14:51:13 +0000
committerKathy Gray2014-11-10 14:51:13 +0000
commit391526a72ca92c05f7735ab90d181c1e840f012c (patch)
tree06e7f844f84d6a1f11c8f7d09f2d35e1ed1cc127 /src/lem_interp
parent2ebd57650a2d0d86c6639783ff6d00c41d6565ac (diff)
Print contents of the [_] hole when it's available.
Also correct makefile typo
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/pretty_interp.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index b201723a..ce7f6e10 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -334,7 +334,10 @@ let doc_exp, doc_let =
string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace)
| E_id id ->
(match id with
- | Id_aux(Id("0"), _) -> (*The evaluation context hole*) doc_id id
+ | Id_aux(Id("0"), _) ->
+ (match Interp.in_lenv env id with
+ | Interp.V_unknown -> doc_id id
+ | v -> string ("\x1b[1;31m[" ^ Interp.string_of_value v ^ "]\x1b[m"))
| _ -> doc_id id)
| E_lit lit -> doc_lit lit
| E_cast(typ,e) ->