merged
authorwenzelm
Thu Oct 27 21:52:44 2016 +0200 (2016-10-27)
changeset 64422efdd4c5daf7d
parent 64418 91eae3a1be51
parent 64421 681fae6b00b5
child 64423 012b64bcd399
merged
     1.1 --- a/src/Pure/Admin/build_history.scala	Thu Oct 27 15:51:54 2016 +0200
     1.2 +++ b/src/Pure/Admin/build_history.scala	Thu Oct 27 21:52:44 2016 +0200
     1.3 @@ -379,7 +379,7 @@
     1.4      progress: Progress = Ignore_Progress,
     1.5      progress_result: (String, Bytes) => Unit = (log_name: String, bytes: Bytes) => (),
     1.6      options: String = "",
     1.7 -    args: String = ""): List[(String, Bytes)] =
     1.8 +    args: String = ""): (List[(String, Bytes)], Process_Result) =
     1.9    {
    1.10      val isabelle_admin = isabelle_repos_self + Path.explode("Admin")
    1.11  
    1.12 @@ -428,12 +428,13 @@
    1.13        result += res
    1.14      }
    1.15  
    1.16 -    ssh.execute(
    1.17 -      ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
    1.18 -        ssh.bash_path(isabelle_repos_other) + " " + args,
    1.19 -      progress_stdout = progress_stdout _,
    1.20 -      progress_stderr = progress.echo(_)).check
    1.21 +    val process_result =
    1.22 +      ssh.execute(
    1.23 +        ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
    1.24 +          ssh.bash_path(isabelle_repos_other) + " " + args,
    1.25 +        progress_stdout = progress_stdout _,
    1.26 +        progress_stderr = progress.echo(_))
    1.27  
    1.28 -    result.toList
    1.29 +    (result.toList, process_result)
    1.30    }
    1.31  }
     2.1 --- a/src/Pure/Isar/proof.ML	Thu Oct 27 15:51:54 2016 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Thu Oct 27 21:52:44 2016 +0200
     2.3 @@ -1163,9 +1163,18 @@
     2.4  
     2.5  local
     2.6  
     2.7 -fun terminal_proof qeds initial terminal =
     2.8 -  proof (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
     2.9 -  #> Seq.the_result "";
    2.10 +fun terminal_proof qeds initial terminal state =
    2.11 +  let
    2.12 +    val ctxt = context_of state;
    2.13 +    val check_closure = Method.check_text ctxt #> Method.map_source (Method.method_closure ctxt);
    2.14 +    val initial' = apfst check_closure initial;
    2.15 +    val terminal' = (apfst o Option.map o apfst) check_closure terminal;
    2.16 +  in
    2.17 +    state
    2.18 +    |> proof (SOME initial')
    2.19 +    |> Seq.maps_results (qeds (#2 (#2 initial), terminal'))
    2.20 +    |> Seq.the_result ""
    2.21 +  end;
    2.22  
    2.23  in
    2.24  
     3.1 --- a/src/Pure/Isar/token.ML	Thu Oct 27 15:51:54 2016 +0200
     3.2 +++ b/src/Pure/Isar/token.ML	Thu Oct 27 21:52:44 2016 +0200
     3.3 @@ -507,8 +507,9 @@
     3.4        SOME {name, ...} => (src, Name_Space.get table name)
     3.5      | NONE =>
     3.6          let
     3.7 -          val (name, x) =
     3.8 -            Name_Space.check (Context.Proof ctxt) table (content_of head, pos_of head);
     3.9 +          val pos = pos_of head;
    3.10 +          val (name, x) = Name_Space.check (Context.Proof ctxt) table (content_of head, pos);
    3.11 +          val _ = Context_Position.report ctxt pos Markup.operator;
    3.12            val kind = Name_Space.kind_of (Name_Space.space_of_table table);
    3.13            fun print ctxt' =
    3.14              Name_Space.markup_extern ctxt' (Name_Space.space_of_table (get_table ctxt')) name;
    3.15 @@ -720,11 +721,15 @@
    3.16  fun syntax_generic scan src context =
    3.17    let
    3.18      val (name, pos) = name_of_src src;
    3.19 +    val old_reports = maps reports_of_value src;
    3.20      val args1 = map init_assignable (args_of_src src);
    3.21      fun reported_text () =
    3.22        if Context_Position.is_visible_generic context then
    3.23 -        ((pos, Markup.operator) :: maps (reports_of_value o closure) args1)
    3.24 -        |> map (fn (p, m) => Position.reported_text p m "")
    3.25 +        let val new_reports = maps (reports_of_value o closure) args1 in
    3.26 +          if old_reports <> new_reports then
    3.27 +            map (fn (p, m) => Position.reported_text p m "") new_reports
    3.28 +          else []
    3.29 +        end
    3.30        else [];
    3.31    in
    3.32      (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of