merged
authorwenzelm
Wed Jan 22 23:19:40 2014 +0100 (2014-01-22)
changeset 551212c9d6d305f14
parent 55117 26385678a8f5
parent 55120 68a829b7f1a4
child 55122 3eb7bcca5b90
merged
     1.1 --- a/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 21:14:27 2014 +0100
     1.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy	Wed Jan 22 23:19:40 2014 +0100
     1.3 @@ -468,8 +468,11 @@
     1.4    example.
     1.5  
     1.6    The rail specification language is quoted here as Isabelle @{syntax
     1.7 -  string}; it has its own grammar given below.
     1.8 +  string} or text @{syntax "cartouche"}; it has its own grammar given
     1.9 +  below.
    1.10  
    1.11 +  \begingroup
    1.12 +  \def\isasymnewline{\isatext{\tt\isacharbackslash<newline>}}
    1.13    @{rail \<open>
    1.14    rule? + ';'
    1.15    ;
    1.16 @@ -483,6 +486,7 @@
    1.17      '@'? (string | @{syntax antiquotation}) |
    1.18      '\<newline>'
    1.19    \<close>}
    1.20 +  \endgroup
    1.21  
    1.22    The lexical syntax of @{text "identifier"} coincides with that of
    1.23    @{syntax ident} in regular Isabelle syntax, but @{text string} uses
     2.1 --- a/src/Pure/Isar/specification.ML	Wed Jan 22 21:14:27 2014 +0100
     2.2 +++ b/src/Pure/Isar/specification.ML	Wed Jan 22 23:19:40 2014 +0100
     2.3 @@ -234,10 +234,12 @@
     2.4  
     2.5  fun gen_abbrev prep mode (raw_var, raw_prop) int lthy =
     2.6    let
     2.7 +    val lthy1 = lthy
     2.8 +      |> Proof_Context.set_syntax_mode mode;
     2.9      val ((vars, [(_, prop)]), _) =
    2.10        prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
    2.11 -        (lthy |> Proof_Context.set_mode Proof_Context.mode_abbrev);
    2.12 -    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy prop));
    2.13 +        (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
    2.14 +    val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
    2.15      val var =
    2.16        (case vars of
    2.17          [] => (Binding.name x, NoSyn)
    2.18 @@ -248,13 +250,12 @@
    2.19                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
    2.20                  Position.here (Binding.pos_of b));
    2.21            in (b, mx) end);
    2.22 -    val lthy' = lthy
    2.23 -      |> Proof_Context.set_syntax_mode mode    (* FIXME ?!? *)
    2.24 +    val lthy2 = lthy1
    2.25        |> Local_Theory.abbrev mode (var, rhs) |> snd
    2.26        |> Proof_Context.restore_syntax_mode lthy;
    2.27  
    2.28 -    val _ = Proof_Display.print_consts int lthy' (K false) [(x, T)];
    2.29 -  in lthy' end;
    2.30 +    val _ = Proof_Display.print_consts int lthy2 (K false) [(x, T)];
    2.31 +  in lthy2 end;
    2.32  
    2.33  val abbreviation = gen_abbrev check_free_spec;
    2.34  val abbreviation_cmd = gen_abbrev read_free_spec;
     3.1 --- a/src/Pure/Thy/thy_syntax.ML	Wed Jan 22 21:14:27 2014 +0100
     3.2 +++ b/src/Pure/Thy/thy_syntax.ML	Wed Jan 22 23:19:40 2014 +0100
     3.3 @@ -158,12 +158,15 @@
     3.4    |> filter (fn (_, tok) => Token.is_proper tok)
     3.5    |> clean;
     3.6  
     3.7 -fun find_file toks =
     3.8 -  rev (clean_tokens toks) |> get_first (fn (i, tok) =>
     3.9 -    if Token.is_name tok then
    3.10 -      SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
    3.11 -        handle ERROR msg => error (msg ^ Token.pos_of tok)
    3.12 -    else NONE);
    3.13 +fun find_file ((_, tok) :: toks) =
    3.14 +      if Token.is_command tok then
    3.15 +        toks |> get_first (fn (i, tok) =>
    3.16 +          if Token.is_name tok then
    3.17 +            SOME (i, (Path.explode (Token.content_of tok), Token.position_of tok))
    3.18 +              handle ERROR msg => error (msg ^ Token.pos_of tok)
    3.19 +          else NONE)
    3.20 +      else NONE
    3.21 +  | find_file [] = NONE;
    3.22  
    3.23  in
    3.24  
    3.25 @@ -171,7 +174,7 @@
    3.26    (case span of
    3.27      Span (Command (cmd, pos), toks) =>
    3.28        if Keyword.is_theory_load cmd then
    3.29 -        (case find_file toks of
    3.30 +        (case find_file (clean_tokens toks) of
    3.31            NONE => error ("Bad file argument of command " ^ quote cmd ^ Position.here pos)
    3.32          | SOME (i, path) =>
    3.33              let
     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Wed Jan 22 21:14:27 2014 +0100
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Jan 22 23:19:40 2014 +0100
     4.3 @@ -235,8 +235,10 @@
     4.4          case t :: ts => t :: clean(ts)
     4.5          case Nil => Nil
     4.6        }
     4.7 -    val clean_tokens = clean(tokens.filter(_.is_proper))
     4.8 -    clean_tokens.reverse.find(_.is_name).map(_.content)
     4.9 +    clean(tokens.filter(_.is_proper)) match {
    4.10 +      case tok :: toks if tok.is_command => toks.find(_.is_name).map(_.content)
    4.11 +      case _ => None
    4.12 +    }
    4.13    }
    4.14  
    4.15    def span_files(syntax: Outer_Syntax, span: List[Token]): List[String] =