src/Pure/Tools/jedit.ML
changeset 61620 01db1bed4487
parent 61617 cd7549cd5fe7
child 61621 70b8085f51b4
     1.1 --- a/src/Pure/Tools/jedit.ML	Tue Nov 10 21:31:14 2015 +0100
     1.2 +++ b/src/Pure/Tools/jedit.ML	Tue Nov 10 21:52:18 2015 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature JEDIT =
     1.6  sig
     1.7 -  val is_action: string -> bool
     1.8 +  val check_action: string * Position.T -> string
     1.9  end;
    1.10  
    1.11  structure JEdit: JEDIT =
    1.12 @@ -44,13 +44,17 @@
    1.13          | _ => [])
    1.14      | (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)));
    1.15  
    1.16 -in
    1.17 -
    1.18  fun is_action a =
    1.19    member (op =) (Lazy.force isabelle_jedit_actions) a orelse
    1.20    member (op =) (Lazy.force isabelle_jedit_dockables) a orelse
    1.21    member (op =) (Lazy.force jedit_actions) a;
    1.22  
    1.23 +in
    1.24 +
    1.25 +fun check_action (a, pos) =
    1.26 +  if is_action a then a
    1.27 +  else error ("Bad jEdit action " ^ quote a ^ Position.here pos);
    1.28 +
    1.29  end;
    1.30  
    1.31  end;