--- a/NEWS Sat Nov 01 14:20:38 2014 +0100
+++ b/NEWS Sat Nov 01 15:01:41 2014 +0100
@@ -190,6 +190,10 @@
* Support for Proof General and Isar TTY loop has been discontinued.
Minor INCOMPATIBILITY.
+* Historical command-line terminator ";" is no longer accepted. Minor
+INCOMPATIBILITY, use "isabelle update_semicolons" to remove obsolete
+semicolons from theory sources.
+
* The Isabelle tool "update_cartouches" changes theory files to use
cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/update_semicolons Sat Nov 01 15:01:41 2014 +0100
@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: remove obsolete semicolons from theory sources
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [FILES|DIRS...]"
+ echo
+ echo " Recursively find .thy files and remove obsolete semicolons."
+ echo
+ echo " Old versions of files are preserved by appending \"~~\"."
+ echo
+ exit 1
+}
+
+
+## process command line
+
+[ "$#" -eq 0 -o "$1" = "-?" ] && usage
+
+SPECS="$@"; shift "$#"
+
+
+## main
+
+find $SPECS -name \*.thy -print0 | \
+ xargs -0 "$ISABELLE_TOOL" java isabelle.Update_Semicolons
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Sat Nov 01 15:01:41 2014 +0100
@@ -31,21 +31,6 @@
"\\isabellestyle"}, see also @{cite "isabelle-sys"}). Experienced
users of Isabelle/Isar may easily reconstruct the lost technical
information, while mere readers need not care about quotes at all.
-
- \medskip Isabelle/Isar input may contain any number of input
- termination characters ``@{verbatim ";"}'' (semicolon) to separate
- commands explicitly. This is particularly useful in interactive
- shell sessions to make clear where the current command is intended
- to end. Otherwise, the interpreter loop will continue to issue a
- secondary prompt ``@{verbatim "#"}'' until an end-of-command is
- clearly recognized from the input syntax, e.g.\ encounter of the
- next command keyword.
-
- More advanced interfaces such as Isabelle/jEdit @{cite "Wenzel:2012"}
- do not require explicit semicolons: command spans are determined by
- inspecting the content of the editor buffer. In the printed
- presentation of Isabelle/Isar documents semicolons are omitted
- altogether for readability.
\<close>
--- a/src/Pure/Isar/outer_syntax.ML Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Sat Nov 01 15:01:41 2014 +0100
@@ -70,33 +70,6 @@
command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
-(* parse command *)
-
-local
-
-fun terminate false = Scan.succeed ()
- | terminate true = Parse.group (fn () => "end of input") (Parse.semicolon >> K ());
-
-fun body cmd (name, _) =
- (case cmd name of
- SOME (Command {int_only, parse, ...}) =>
- Parse.!!! (Parse.tags |-- parse >> pair int_only)
- | NONE =>
- Scan.succeed (false, Toplevel.imperative (fn () =>
- error ("Bad parser for outer syntax command " ^ quote name))));
-
-in
-
-fun parse_command do_terminate cmd =
- Parse.semicolon >> K NONE ||
- (Parse.position Parse.command :-- body cmd) --| terminate do_terminate
- >> (fn ((name, pos), (int_only, f)) =>
- SOME (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
- Toplevel.interactive int_only |> f));
-
-end;
-
-
(* type outer_syntax *)
datatype outer_syntax = Outer_Syntax of
@@ -227,24 +200,35 @@
(** toplevel parsing **)
-(* basic sources *)
+(* parse commands *)
+
+local
-fun toplevel_source term do_recover cmd src =
- let
- val no_terminator = Scan.unless Parse.semicolon (Scan.one Token.not_eof);
- fun recover int = (int, fn _ => Scan.repeat no_terminator >> K [NONE]);
- in
- src
- |> Token.source_proper
- |> Source.source Token.stopper
- (Scan.bulk (Parse.$$$ "--" -- Parse.!!! Parse.document_source >> K NONE || Parse.not_eof >> SOME))
- (Option.map recover do_recover)
- |> Source.map_filter I
- |> Source.source Token.stopper
- (Scan.bulk (fn xs => Parse.!!! (parse_command term (cmd ())) xs))
- (Option.map recover do_recover)
- |> Source.map_filter I
- end;
+fun parse_command outer_syntax =
+ Parse.position Parse.command :|-- (fn (name, pos) =>
+ let
+ val tr0 = Toplevel.empty |> Toplevel.name name |> Toplevel.position pos;
+ in
+ (case lookup_commands outer_syntax name of
+ SOME (Command {int_only, parse, ...}) =>
+ Parse.!!! (Parse.tags |-- parse) >> (fn f => tr0 |> Toplevel.interactive int_only |> f)
+ | NONE =>
+ Scan.succeed
+ (tr0 |> Toplevel.imperative (fn () =>
+ error ("Bad parser for outer syntax command " ^ quote name ^ Position.here pos))))
+ end);
+
+val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
+
+in
+
+fun commands_source outer_syntax =
+ Token.source_proper #>
+ Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) NONE #>
+ Source.map_filter I #>
+ Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command outer_syntax) xs)) NONE;
+
+end;
(* off-line scanning/parsing *)
@@ -259,7 +243,7 @@
Source.of_string str
|> Symbol.source
|> Token.source {do_recover = SOME false} (K lexs) pos
- |> toplevel_source false NONE (K (lookup_commands syntax))
+ |> commands_source syntax
|> Source.exhaust;
@@ -317,7 +301,7 @@
fun read_spans outer_syntax toks =
Source.of_list toks
- |> toplevel_source false NONE (K (lookup_commands outer_syntax))
+ |> commands_source outer_syntax
|> Source.exhaust;
end;
--- a/src/Pure/Isar/parse.ML Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Isar/parse.ML Sat Nov 01 15:01:41 2014 +0100
@@ -39,7 +39,6 @@
val keyword_improper: string -> string parser
val $$$ : string -> string parser
val reserved: string -> string parser
- val semicolon: string parser
val underscore: string parser
val maybe: 'a parser -> 'a option parser
val tag_name: string parser
@@ -216,8 +215,6 @@
group (fn () => "reserved identifier " ^ quote x)
(RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
-val semicolon = $$$ ";";
-
val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
fun maybe scan = underscore >> K NONE || scan >> SOME;
--- a/src/Pure/Isar/parse.scala Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Isar/parse.scala Sat Nov 01 15:01:41 2014 +0100
@@ -39,13 +39,7 @@
}
val token = in.first
if (pred(token)) Success((token, pos), proper(in.rest))
- else
- token.text match {
- case (txt, "") =>
- Failure(s + " expected,\nbut " + txt + " was found", in)
- case (txt1, txt2) =>
- Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
- }
+ else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
}
}
}
--- a/src/Pure/Isar/token.ML Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Isar/token.ML Sat Nov 01 15:01:41 2014 +0100
@@ -44,7 +44,6 @@
val is_name: T -> bool
val is_proper: T -> bool
val is_improper: T -> bool
- val is_semicolon: T -> bool
val is_comment: T -> bool
val is_begin_ignore: T -> bool
val is_end_ignore: T -> bool
@@ -233,9 +232,6 @@
val is_improper = not o is_proper;
-fun is_semicolon (Token (_, (Keyword, ";"), _)) = true
- | is_semicolon _ = false;
-
fun is_comment (Token (_, (Comment, _), _)) = true
| is_comment _ = false;
@@ -341,18 +337,16 @@
fun print tok = Markup.markup (markup tok) (unparse tok);
fun text_of tok =
- if is_semicolon tok then ("terminator", "")
- else
- let
- val k = str_of_kind (kind_of tok);
- val m = markup tok;
- val s = unparse tok;
- in
- if s = "" then (k, "")
- else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
- then (k ^ " " ^ Markup.markup m s, "")
- else (k, Markup.markup m s)
- end;
+ let
+ val k = str_of_kind (kind_of tok);
+ val m = markup tok;
+ val s = unparse tok;
+ in
+ if s = "" then (k, "")
+ else if size s < 40 andalso not (exists_string (fn c => c = "\n") s)
+ then (k ^ " " ^ Markup.markup m s, "")
+ else (k, Markup.markup m s)
+ end;
--- a/src/Pure/Isar/token.scala Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Isar/token.scala Sat Nov 01 15:01:41 2014 +0100
@@ -202,9 +202,5 @@
else if (kind == Token.Kind.CARTOUCHE) Scan.Parsers.cartouche_content(source)
else if (kind == Token.Kind.COMMENT) Scan.Parsers.comment_content(source)
else source
-
- def text: (String, String) =
- if (is_keyword && source == ";") ("terminator", "")
- else (kind.toString, source)
}
--- a/src/Pure/Thy/latex.ML Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Thy/latex.ML Sat Nov 01 15:01:41 2014 +0100
@@ -119,11 +119,9 @@
(* token output *)
-val invisible_token = Token.keyword_with (fn s => s = ";") orf Token.is_kind Token.Comment;
-
fun output_basic tok =
let val s = Token.content_of tok in
- if invisible_token tok then ""
+ if Token.is_kind Token.Comment tok then ""
else if Token.is_command tok then
"\\isacommand{" ^ output_syms s ^ "}"
else if Token.is_kind Token.Keyword tok andalso Symbol.is_ascii_identifier s then
--- a/src/Pure/Thy/thy_header.ML Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Thy/thy_header.ML Sat Nov 01 15:01:41 2014 +0100
@@ -74,7 +74,7 @@
val header_lexicons =
pairself (Scan.make_lexicon o map Symbol.explode)
- (["%", "(", ")", ",", "::", ";", "==", "and", beginN, importsN, keywordsN],
+ (["%", "(", ")", ",", "::", "==", "and", beginN, importsN, keywordsN],
[headerN, theoryN]);
@@ -120,8 +120,7 @@
val header =
(Parse.command_name headerN -- Parse.tags) |--
- (Parse.!!! (Parse.document_source -- Scan.repeat Parse.semicolon --
- (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
+ (Parse.!!! (Parse.document_source -- (Parse.command_name theoryN -- Parse.tags) |-- args)) ||
(Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
fun token_source pos str =
--- a/src/Pure/Thy/thy_header.scala Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Thy/thy_header.scala Sat Nov 01 15:01:41 2014 +0100
@@ -23,7 +23,7 @@
val BEGIN = "begin"
private val lexicon =
- Scan.Lexicon("%", "(", ")", ",", "::", ";", "==",
+ Scan.Lexicon("%", "(", ")", ",", "::", "==",
AND, BEGIN, HEADER, IMPORTS, KEYWORDS, THEORY)
@@ -75,8 +75,7 @@
{ case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
(keyword(HEADER) ~ tags) ~!
- ((document_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^
- { case _ ~ x => x } |
+ ((document_source ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
(keyword(THEORY) ~ tags) ~! args ^^ { case _ ~ x => x }
}
--- a/src/Pure/Thy/thy_output.ML Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Sat Nov 01 15:01:41 2014 +0100
@@ -413,7 +413,6 @@
make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
val spans = toks
- |> filter_out Token.is_semicolon
|> take_suffix Token.is_space |> #1
|> Source.of_list
|> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/update_semicolons.scala Sat Nov 01 15:01:41 2014 +0100
@@ -0,0 +1,34 @@
+/* Title: Pure/Tools/update_semicolons.scala
+ Author: Makarius
+
+Remove obsolete semicolons from theory sources.
+*/
+
+package isabelle
+
+
+object Update_Semicolons
+{
+ def update_semicolons(path: Path)
+ {
+ val text0 = File.read(path)
+ val text1 =
+ (for (tok <- Outer_Syntax.empty.scan(text0).iterator if tok.source != ";")
+ yield tok.source).mkString
+
+ if (text0 != text1) {
+ Output.writeln("changing " + path)
+ File.write_backup2(path, text1)
+ }
+ }
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool0 {
+ args.foreach(arg => update_semicolons(Path.explode(arg)))
+ }
+ }
+}
--- a/src/Pure/build-jars Sat Nov 01 14:20:38 2014 +0100
+++ b/src/Pure/build-jars Sat Nov 01 15:01:41 2014 +0100
@@ -96,6 +96,7 @@
Tools/simplifier_trace.scala
Tools/task_statistics.scala
Tools/update_cartouches.scala
+ Tools/update_semicolons.scala
library.scala
term.scala
term_xml.scala