merged

--- a/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 21:14:27 2014 +0100
+++ b/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 23:19:40 2014 +0100
@@ -468,8 +468,11 @@
   example.
 
   The rail specification language is quoted here as Isabelle @{syntax
-  string}; it has its own grammar given below.
+  string} or text @{syntax "cartouche"}; it has its own grammar given
+  below.
 
+  \begingroup
+  \def\isasymnewline{\isatext{\tt\isacharbackslash<newline>}}
   @{rail \<open>
   rule? + ';'
   ;
@@ -483,6 +486,7 @@
     '@'? (string | @{syntax antiquotation}) |
     '\<newline>'
   \<close>}
+  \endgroup
 
   The lexical syntax of @{text "identifier"} coincides with that of
   @{syntax ident} in regular Isabelle syntax, but @{text string} uses

--- a/src/Pure/Isar/specification.ML	Wed Jan 22 21:14:27 2014 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Jan 22 23:19:40 2014 +0100
@@ -234,10 +234,12 @@
 
 fun gen_abbrev prep mode (raw_var, raw_prop) int lthy =
   let
+    val lthy1 = lthy
+      |> Proof_Context.set_syntax_mode mode;
     val ((vars, [(_, prop)]), _) =
       prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
-        (lthy |> Proof_Context.set_mode Proof_Context.mode_abbrev);
-    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy prop));
+        (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
+    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
     val var =
       (case vars of
         [] => (Binding.name x, NoSyn)
@@ -248,13 +250,12 @@
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.here (Binding.pos_of b));
           in (b, mx) end);
-    val lthy' = lthy
-      |> Proof_Context.set_syntax_mode mode    (* FIXME ?!? *)
+    val lthy2 = lthy1
       |> Local_Theory.abbrev mode (var, rhs) |> snd
       |> Proof_Context.restore_syntax_mode lthy;
 
-    val _ = Proof_Display.print_consts int lthy' (K false) [(x, T)];
-  in lthy' end;
+    val _ = Proof_Display.print_consts int lthy2 (K false) [(x, T)];
+  in lthy2 end;
 
 val abbreviation = gen_abbrev check_free_spec;
 val abbreviation_cmd = gen_abbrev read_free_spec;

--- a/src/Pure/Thy/thy_syntax.ML	Wed Jan 22 21:14:27 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Jan 22 23:19:40 2014 +0100
@@ -158,12 +158,15 @@
   |> filter (fn (_, tok) => Token.is_proper tok)
   |> clean;
 
-fun find_file toks =
-  rev (clean_tokens toks) |> get_first (fn (i, tok) =>
-    if Token.is_name tok then
-      SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
-        handle ERROR msg => error (msg ^ Token.pos_of tok)
-    else NONE);
+fun find_file ((_, tok) :: toks) =
+      if Token.is_command tok then
+        toks |> get_first (fn (i, tok) =>
+          if Token.is_name tok then
+            SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
+              handle ERROR msg => error (msg ^ Token.pos_of tok)
+          else NONE)
+      else NONE
+  | find_file [] = NONE;
 
 in
 
@@ -171,7 +174,7 @@
   (case span of
     Span (Command (cmd, pos), toks) =>
       if Keyword.is_theory_load cmd then
-        (case find_file toks of
+        (case find_file (clean_tokens toks) of
           NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
         | SOME (i, path) =>
             let

--- a/src/Pure/Thy/thy_syntax.scala	Wed Jan 22 21:14:27 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Jan 22 23:19:40 2014 +0100
@@ -235,8 +235,10 @@
         case t :: ts => t :: clean(ts)
         case Nil => Nil
       }
-    val clean_tokens = clean(tokens.filter(_.is_proper))
-    clean_tokens.reverse.find(_.is_name).map(_.content)
+    clean(tokens.filter(_.is_proper)) match {
+      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
+      case _ => None
+    }
   }
 
   def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =