src/Pure/ProofGeneral/proof_general_emacs.ML
changeset 25630 98dd706319a1
parent 25553 06ffd67a5e79
child 25749 10e7feb4e595
equal deleted inserted replaced
25629:f7c6ca73a8bd 25630:98dd706319a1
    98 
    98 
    99 
    99 
   100 (* common markup *)
   100 (* common markup *)
   101 
   101 
   102 fun proof_general_markup (name, props) =
   102 fun proof_general_markup (name, props) =
   103   (if name = Markup.promptN then ("", special "372")
   103   let
   104     else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
   104     val (bg1, en1) =
   105     else if name = Markup.sendbackN then (special "376", special "377")
   105       if name = Markup.promptN then ("", special "372")
   106     else if name = Markup.hiliteN then (special "327", special "330")
   106       else if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
   107     else ("", ""))
   107       else if name = Markup.sendbackN then (special "376", special "377")
   108   |> (name <> Markup.promptN andalso print_mode_active IsabelleProcess.test_markupN) ?
   108       else if name = Markup.hiliteN then (special "327", special "330")
   109       (fn (bg1, en1) =>
   109       else ("", "");
   110         let val (bg2, en2) = IsabelleProcess.test_markup (name, props)
   110     val (bg2, en2) =
   111         in (bg1 ^ bg2, en2 ^ en1) end);
   111       if name <> Markup.promptN andalso print_mode_active IsabelleProcess.test_markupN
       
   112       then IsabelleProcess.test_markup (name, props)
       
   113       else ("", "");
       
   114   in (bg1 ^ bg2, en2 ^ en1) end;
   112 
   115 
   113 val _ = Markup.add_mode proof_generalN proof_general_markup;
   116 val _ = Markup.add_mode proof_generalN proof_general_markup;
   114 
   117 
   115 
   118 
   116 (* messages and notification *)
   119 (* messages and notification *)