Add position info to module doc

Stream: lean4

[Xubai Wang]

Lean support multiple module doc like this. But the current module doc implementation is

private builtin_initialize moduleDocExt : SimplePersistentEnvExtension String (Std.PersistentArray String) ← registerSimplePersistentEnvExtension {
  name          := `moduleDocExt
  addImportedFn := fun _ => {}
  addEntryFn    := fun s e => s.push e
  toArrayFn     := fun es => es.toArray
}

which ignores the position info, and we cannot get the module docs to the right place.

[Xubai Wang]

I made a few modifications to Lean 4 docstring modules in this commit, in order to support positioned mod doc.

May I open a pull request directly? Or is there any other prerequisites?