# HG changeset patch
# User wenzelm
# Date 1373491810 -7200
# Node ID ff525a38dba90bc91004c685d132a427adfde570
# Parent  5cad4a5f5615bb0cf7fdd08d2f7276ce298218a8
added "echo" command for demonstration purposes;

diff -r 5cad4a5f5615 -r ff525a38dba9 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Wed Jul 10 23:25:28 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML	Wed Jul 10 23:30:10 2013 +0200
@@ -8,6 +8,9 @@
 struct
 
 val _ =
+  Isabelle_Process.protocol_command "echo" (fn args => List.app writeln args);
+
+val _ =
   Isabelle_Process.protocol_command "Document.define_command"
     (fn [id, name, text] =>
       Document.change_state (Document.define_command (Document_ID.parse id) name text));