--- a/src/Pure/PIDE/command.ML Sat Apr 07 18:08:29 2012 +0200
+++ b/src/Pure/PIDE/command.ML Sat Apr 07 19:28:44 2012 +0200
@@ -6,7 +6,6 @@
signature COMMAND =
sig
- val parse_command: string -> string -> Token.T list
type 'a memo
val memo: (unit -> 'a) -> 'a memo
val memo_value: 'a -> 'a memo
@@ -18,17 +17,6 @@
structure Command: COMMAND =
struct
-(* parse command *)
-
-fun parse_command id text =
- Position.setmp_thread_data (Position.id_only id)
- (fn () =>
- let
- val toks = Thy_Syntax.parse_tokens (#1 (Outer_Syntax.get_syntax ())) (Position.id id) text;
- val _ = Output.status (Markup.markup_only Isabelle_Markup.parsed);
- in toks end) ();
-
-
(* memo results *)
datatype 'a expr =