# HG changeset patch
# User wenzelm
# Date 1414850501 -3600
# Node ID 5ff61774df1103e65a892f9e26cd1989ce5edb59
# Parent  fee7cfa69c507655d6e3096e70710f9d553dddba
command-line terminator ";" is no longer accepted;

diff -r fee7cfa69c50 -r 5ff61774df11 NEWS
--- 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.
 
diff -r fee7cfa69c50 -r 5ff61774df11 lib/Tools/update_semicolons
--- /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
diff -r fee7cfa69c50 -r 5ff61774df11 src/Doc/Isar_Ref/Outer_Syntax.thy
--- 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>
 
 
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Isar/outer_syntax.ML
--- 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;
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Isar/parse.ML
--- 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;
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Isar/parse.scala
--- 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)
           }
         }
       }
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Isar/token.ML
--- 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;
 
 
 
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Isar/token.scala
--- 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)
 }
 
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Thy/latex.ML
--- 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
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Thy/thy_header.ML
--- 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 =
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Thy/thy_header.scala
--- 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 }
   }
 
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Thy/thy_output.ML
--- 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
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/Tools/update_semicolons.scala
--- /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)))
+    }
+  }
+}
diff -r fee7cfa69c50 -r 5ff61774df11 src/Pure/build-jars
--- 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