src/Doc/antiquote_setup.ML
changeset 56294 85911b8a6868
parent 56278 2576d3a40ed6
child 56304 40274e4f5ebf
     1.1 --- a/src/Doc/antiquote_setup.ML	Wed Mar 26 14:15:34 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Wed Mar 26 14:41:52 2014 +0100
     1.3 @@ -192,17 +192,17 @@
     1.4  
     1.5  fun no_check _ _ = true;
     1.6  
     1.7 -fun check_command (name, pos) =
     1.8 +fun check_command ctxt (name, pos) =
     1.9    is_some (Keyword.command_keyword name) andalso
    1.10      let
    1.11        val markup =
    1.12          Outer_Syntax.scan Position.none name
    1.13          |> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ())))
    1.14          |> map (snd o fst);
    1.15 -      val _ = List.app (Position.report pos) markup;
    1.16 +      val _ = Context_Position.reports ctxt (map (pair pos) markup);
    1.17      in true end;
    1.18  
    1.19 -fun check_tool (name, pos) =
    1.20 +fun check_tool ctxt (name, pos) =
    1.21    let
    1.22      fun tool dir =
    1.23        let val path = Path.append dir (Path.basic name)
    1.24 @@ -210,7 +210,7 @@
    1.25    in
    1.26      (case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of
    1.27        NONE => false
    1.28 -    | SOME path => (Position.report pos (Markup.path (Path.implode path)); true))
    1.29 +    | SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true))
    1.30    end;
    1.31  
    1.32  val arg = enclose "{" "}" o clean_string;
    1.33 @@ -255,7 +255,7 @@
    1.34  val _ =
    1.35    Theory.setup
    1.36     (entity_antiqs no_check "" @{binding syntax} #>
    1.37 -    entity_antiqs (K check_command) "isacommand" @{binding command} #>
    1.38 +    entity_antiqs check_command "isacommand" @{binding command} #>
    1.39      entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #>
    1.40      entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #>
    1.41      entity_antiqs (can o Method.check_name) "" @{binding method} #>
    1.42 @@ -269,7 +269,7 @@
    1.43      entity_antiqs no_check "isatt" @{binding system_option} #>
    1.44      entity_antiqs no_check "" @{binding inference} #>
    1.45      entity_antiqs no_check "isatt" @{binding executable} #>
    1.46 -    entity_antiqs (K check_tool) "isatool" @{binding tool} #>
    1.47 +    entity_antiqs check_tool "isatool" @{binding tool} #>
    1.48      entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #>
    1.49      entity_antiqs (K (is_action o #1)) "isatt" @{binding action});
    1.50