Add widget effect support for specifying location of text to insert.

[EdAyers]

See leanprover-community/lean#501
and https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/paste.20the.20goal.20at.20the.20cursor

This commit allows insert_text effects to include position information. An insert_text effect now has two extra fields:

{ "kind": "insert_text"
, "line": number // the line number to insert at, can be negative for relative line_type
, "column"?: number
, "file_name"?: string
, "insert_type": "absolute" | "relative" // whether line property is relative to cursor or absolute
, "text": string
}