# HG changeset patch # User wenzelm # Date 918491604 -3600 # Node ID aaabe48bafcb13ff39ed0e25ec3967dedc835d15 # Parent 87e5f5b4059547828a3afb8b1b1a6d3c9a4732ba "files" keyword! diff -r 87e5f5b40595 -r aaabe48bafcb src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Feb 08 17:33:03 1999 +0100 +++ b/src/Pure/Isar/isar_syn.ML Mon Feb 08 17:33:24 1999 +0100 @@ -210,7 +210,7 @@ (* use ML text *) val useP = - OuterSyntax.parser true "use" "eval ML text from file" + OuterSyntax.parser false "use" "eval ML text from file" (name >> IsarCmd.use); val mlP = @@ -511,7 +511,7 @@ val keywords = ["(", ")", "*", "+", "--", ",", ":", "::", ";", "<", "<=", "=", "==", "=>", - "?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is", + "?", "[", "]", "and", "as", "binder", "files", "infixl", "infixr", "is", "output", "{", "|", "}"]; val parsers = [