From fdcd31d4ef474b4a7217aa65c239e6e271a35754 Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Mon, 20 Aug 2007 09:38:10 +0000
Subject: proper use of ProofGeneral.sendback;

---
 etc/isar/Sendback.thy | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

diff --git a/etc/isar/Sendback.thy b/etc/isar/Sendback.thy
index 345064a0..5d0ac019 100644
--- a/etc/isar/Sendback.thy
+++ b/etc/isar/Sendback.thy
@@ -1,17 +1,11 @@
-(* Demonstrate the use of literal command markup *)
+(* $Id$ *)
 
-theory Sendback imports Main begin
+header {* Demonstrate the use of literal command markup *}
 
-ML {* val pgasciiN = "PGASCII";
-fun special oct =
-  if print_mode_active pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
-  else oct_char oct; 
-fun sendback cmd = writeln ("Try this: \n   " ^ (special "376") ^ cmd ^ (special "377") ^ "\n\n")
-*}
+theory Sendback imports Main begin
 
 ML {*
-fun sendback2 cmd = (writeln "Try this: "; 
-		    ProofGeneral.sendback cmd [])
+fun sendback cmd = ProofGeneral.sendback "Try this:" [Pretty.str cmd]
 *}
 
 theorem and_comms: "A & B --> B & A"
-- 
cgit v1.2.3