General modern "quotation" syntax support

[mn200]

Suggestion from @myreen on Discord:

Could there be general-purpose quote filter support for making this nicer? Specifics can be discussed, but something along these lines:

val cakeml_code = append_prog o process_topdecs;

Quote cakeml_code:
  fun b_inputAllTokens c0 is f g =
    b_inputAllTokens_aux c0 is f g []
End

Quote cakeml_code:
  fun b_inputAllTokensFrom c0 fname f g =
    let
      val is = b_openIn fname
      val lines = b_inputAllTokens c0 is f g
    in
      b_closeIn is; Some lines
    end handle BadFileName => None
End

I can't quite decide what the syntax should be if one also wants to bind the result of applying the function... Perhaps:

Quote cake_ast = process_topdecs:
  fun b_inputAllTokens c0 is f g =
    b_inputAllTokens_aux c0 is f g []
End