- Modified brace printing behaviour.

src/latex.c

@@ -91,7 +91,7 @@ latexDone (const System sys)
 //! Print a term using LaTeX and highlighting.
 /**
  * Basically a recode of termPrint, now specific using latex codes and with a
- * highlighting feature.
+ * highlighting feature. There is still some obsolete code to show variable mappings in a term.
  *@param term a term to be printed.
  *@param highlight a list of terms to be highlighted.
  */
@@ -134,15 +134,7 @@ latexTermPrint (Term term, Termlist highlight)
   if (realTermTuple (term))
     {
       printf ("(");
-      while (realTermTuple (term))
+      latexTermTuplePrint (term);
-	{
-	  latexTermPrint (term->op1, highlight);
-	  printf (",");
-	  term = term->op2;
-	  if (!realTermTuple (term))
-	    latexTermPrint (term, highlight);
-
-	}
       printf (")");
       return;
     }
@@ -154,14 +146,14 @@ latexTermPrint (Term term, Termlist highlight)
 	  /* function application */
 	  latexTermPrint (term->key, highlight);
 	  printf ("(");
-	  latexTermPrint (term->op, highlight);
+	  latexTermTuplePrint (term->op, highlight);
 	  printf (")");
 	}
       else
 	{
 	  /* normal encryption */
 	  printf ("\\{");
-	  latexTermPrint (term->op, highlight);
+	  latexTermTuplePrint (term->op, highlight);
 	  printf ("\\}_{");
 	  latexTermPrint (term->key, highlight);
 	  printf ("}");
@@ -169,6 +161,32 @@ latexTermPrint (Term term, Termlist highlight)
     }
 }
 
+//! Print an inner (tuple) term using LaTeX, without brackets.
+/**
+ * The tuple printing only works correctly for normalized terms.
+ * If not, they might are displayed as "((x,y),z)". Maybe that is even
+ * desirable to distinguish them.
+ */
+void
+latexTermTuplePrint (Term term, Termlist hl)
+{
+  if (term == NULL)
+    {
+      printf ("Empty term");
+      return;
+    }
+  term = deVar(term);
+  while (realTermTuple (term))
+    {
+      // To remove any brackets, change this into latexTermTuplePrint.
+      latexTermPrint (term->op1, hl);
+      printf (",");
+      term = deVar(term->op2);
+    }
+  latexTermPrint(term, hl);
+  return;
+}
+
 //! Print a termlist in LaTeX using highlighting.
 /**
  * Extending LaTeX term printing to term list printing, again with highlight

src/latex.h

@@ -17,5 +17,7 @@ void latexMessagePrint(const System sys, int from, int to);
 void latexLearnComment(const System sys, Termlist tl);
 void latexTracePrint(System sys);
 void attackDisplayLatex(System sys);
+void latexTermPrint (Term term, Termlist hl);
+void latexTermTuplePrint (Term term, Termlist hl);
 
 #endif

src/terms.c

@@ -231,6 +231,12 @@ termOccurs (Term t, Term tsub)
 }
 
 //! Print a term to stdout.
+/**
+ * The tuple printing only works correctly for normalized terms.
+ * If not, they might are displayed as "((x,y),z)". Maybe that is even
+ * desirable to distinguish them.
+ *\sa termTuplePrint()
+ */
 void
 termPrint (Term term)
 {
@@ -271,15 +277,7 @@ termPrint (Term term)
   if (realTermTuple (term))
     {
       printf ("(");
-      while (realTermTuple (term))
+      termTuplePrint(term);
-	{
-	  termPrint (term->op1);
-	  printf (",");
-	  term = term->op2;
-	  if (!realTermTuple (term))
-	    termPrint (term);
-
-	}
       printf (")");
       return;
     }
@@ -291,7 +289,7 @@ termPrint (Term term)
 	  /* function application */
 	  termPrint (term->key);
 	  printf ("(");
-	  termPrint (term->op);
+	  termTuplePrint (term->op);
 	  printf (")");
 	}
       else
@@ -300,7 +298,7 @@ termPrint (Term term)
 	  if (globalLatex)
 	    {
 	      printf ("\\{");
-	      termPrint (term->op);
+	      termTuplePrint (term->op);
 	      printf ("\\}_{");
 	      termPrint (term->key);
 	      printf ("}");
@@ -308,7 +306,7 @@ termPrint (Term term)
 	  else
 	    {
 	      printf ("{");
-	      termPrint (term->op);
+	      termTuplePrint (term->op);
 	      printf ("}");
 	      termPrint (term->key);
 	    }
@@ -316,6 +314,31 @@ termPrint (Term term)
     }
 }
 
+//! Print an inner (tuple) term to stdout, without brackets.
+/**
+ * The tuple printing only works correctly for normalized terms.
+ * If not, they might are displayed as "((x,y),z)". Maybe that is even
+ * desirable to distinguish them.
+ */
+void
+termTuplePrint (Term term)
+{
+  if (term == NULL)
+    {
+      printf ("Empty term");
+      return;
+    }
+  term = deVar(term);
+  while (realTermTuple (term))
+    {
+      // To remove any brackets, change this into termTuplePrint.
+      termPrint (term->op1);
+      printf (",");
+      term = deVar(term->op2);
+    }
+  termPrint(term);
+  return;
+}
 
 //! Make a deep copy of a term.
 /**

src/terms.h

@@ -101,6 +101,7 @@ int hasTermVariable (Term term);
 int isTermEqualFn (Term term1, Term term2);
 int termOccurs (Term t, Term tsub);
 void termPrint (Term term);
+void termTuplePrint (Term term);
 Term termDuplicate (const Term term);
 Term termDuplicateDeep (const Term term);
 Term termDuplicateUV (Term term);