added backquote;
authorwenzelm
Sat, 07 Jan 2006 12:26:27 +0100
changeset 18603 04c2c702a3fb
parent 18602 8f25a0f7f446
child 18604 4000f368dc7f
added backquote;
src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Jan 07 12:26:25 2006 +0100
+++ b/src/Pure/General/pretty.ML	Sat Jan 07 12:26:27 2006 +0100
@@ -33,6 +33,7 @@
   val blk: int * T list -> T
   val unbreakable: T -> T
   val quote: T -> T
+  val backquote: T -> T
   val commas: T list -> T list
   val breaks: T list -> T list
   val fbreaks: T list -> T list
@@ -204,8 +205,8 @@
 
 (* utils *)
 
-fun quote prt =
-  blk (1, [str "\"", prt, str "\""]);
+fun quote prt = blk (1, [str "\"", prt, str "\""]);
+fun backquote prt = blk (1, [str "`", prt, str "`"]);
 
 fun separate_pretty sep prts =
   prts