Give annotations to record field names that appear in updates.

Field names in selections were already annotated. Closes #191
HOL-Theorem-Prover · Aug 29, 2014 · ff0ad49 · ff0ad49
1 parent 4f16bf9
commit ff0ad49
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 1 deletion.
diff --git a/src/TeX/theory_tests/expected-output b/src/TeX/theory_tests/expected-output
@@ -15,3 +15,11 @@
   \HOLTokenBar{} \HOLConst{Tyrep} \HOLTyOp{string} \HOLTyOp{term}
 
 \HOLinline{\HOLFreeVar{x}.\HOLFieldName{fld1}}
+
+\HOLinline{\HOLFreeVar{x} with \HOLFieldName{fld1} := \HOLConst{T}}
+
+\HOLinline{\HOLFreeVar{x} with \HOLTokenLeftrec{}\HOLFieldName{fld1} := \HOLConst{T}; \HOLFieldName{fld2} := \HOLConst{K} \HOLNumLit{3}\HOLTokenRightrec{}}
+
+\HOLinline{\HOLFreeVar{x} with \HOLFieldName{fld1} updated_by (\HOLConst{\HOLTokenNeg{}})}
+
+\HOLinline{\HOLFreeVar{x} with \HOLFieldName{fld2} updated_by \HOLFreeVar{g}}
diff --git a/src/TeX/theory_tests/input b/src/TeX/theory_tests/input
@@ -1,3 +1,11 @@
 \HOLthm{mdt.datatype_term}
 
 \HOLtm{x.fld1}
+
+\HOLtm{x with fld1 := T}
+
+\HOLtm{x with <| fld1 := T; fld2 := K 3 |>}
+
+\HOLtm{x with fld1 updated_by $~}
+
+\HOLtm{x with <| fld2 updated_by g |>}
diff --git a/src/parse/term_pp.sml b/src/parse/term_pp.sml
@@ -1035,7 +1035,8 @@ fun pp_term (G : grammar) TyG backend = let
                 else valOf recfupd_info
             in
               block INCONSISTENT 2
-                    (add_string fld >>
+                    (add_ann_string
+                       (fld, PPBackEnd.Literal PPBackEnd.FldName) >>
                      add_string " " >>
                      add_string updtok >>
                      add_break(1,0) >>