--- a/src/Pure/Isar/token.ML Tue Nov 19 13:54:02 2013 +0100
+++ b/src/Pure/Isar/token.ML Tue Nov 19 19:33:27 2013 +0100
@@ -46,7 +46,7 @@
val content_of: T -> string
val unparse: T -> string
val text_of: T -> string * string
- val get_files: T -> file list option
+ val get_files: T -> file list
val put_files: file list -> T -> T
val get_value: T -> value option
val map_value: (value -> value) -> T -> T
@@ -244,10 +244,11 @@
(* inlined file content *)
-fun get_files (Token (_, _, Value (SOME (Files files)))) = SOME files
- | get_files _ = NONE;
+fun get_files (Token (_, _, Value (SOME (Files files)))) = files
+ | get_files _ = [];
-fun put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
+fun put_files [] tok = tok
+ | put_files files (Token (x, y, Slot)) = Token (x, y, Value (SOME (Files files)))
| put_files _ tok =
raise Fail ("Cannot put inlined files here" ^ Position.here (position_of tok));